Naming: ne_zero vs nonzero

Stream: mathlib4

[Jovan Gerbscheid]

Both ne_zero and nonzero are used as spellings for _ ≠ 0. Is this a problem, and do we have a preferred option?

[Etienne Marion]

I think ne_zero is better.

[Ruben Van de Velde]

Found 323 declarations whose name contains "nonzero". :scream:

[Ruben Van de Velde]

Though a fair number of false positives

[Ruben Van de Velde]

Most of them, even

[Robin Arnez]

I think
@loogle "ne_zero", _ ≠ 0

[loogle]

:search: Nat.succ_ne_zero, Nat.one_ne_zero, and 1488 more

[Damiano Testa]

$ (git grep "\(theorem\|lemma\|inductive\|structure\|def\|class\|instance\|alias\|abbrev\) [^ ]*nonzero" *) | wc
     91    1252   11655

[Robin Arnez]

is clearly more popular than
@loogle "nonzero", _ ≠ 0

[loogle]

:search: Int.natAbs_sign_of_nonzero, Int.sign_ofNat_of_nonzero, and 137 more

[Ruben Van de Velde]

I'll fix the three Int ones now

[Ruben Van de Velde]

Oh, the first two are in core. I'll fix the one

[Damiano Testa]

I didn't know that docs#List.nonzeroMinimum existed.

[Markus Himmel]

This seems to be an implementation detail of the omega tactic, it should be moved out of the List namespace.

[Kim Morrison]

lean#10243