spelling convention for "nonzero"

Stream: mathlib4

[Alex Meiburg]

I'm aware of theorems spelling it as "nonzero", "nonZero", "non_zero", "neZero", and "ne_zero". The second option is mostly confined to the NeZero structure, but not entirely, e.g. LinearEquiv.smulOfNeZero and unitsEquivNeZero

examples:

• docs#mul_ne_zero_iff
• docs#div_ne_zero_iff
• docs#pos_of_ne_zero
• IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
• Polynomial.natDegree_mem_support_of_nonzero
• Ideal.exists_nonzero_mem_of_ne_bot
• Units.orbitRel_nonZero_iff
• NumberField.det_of_basisMatrix_non_zero
• Matrix.IsHermitian.rank_eq_card_non_zero_eigs

I also found Algebra.discr_not_zero_of_basis but I think that one is just objectively a wrong name. :)

The pos/neg/nonneg/nonpos convention fixes this for other relations, but maybe it would be good to fix this for nonequality?

[Yaël Dillies]

Just use ne_zero please (except for uses of NeZero which should become neZero by the convention)

[Alex Meiburg]

https://github.com/leanprover-community/leanprover-community.github.io/pull/789, then?

[Ruben Van de Velde]

(And fooNeZero / neZeroFoo are correct for defs)

[Andrew Yang]

Do we really want to mention every non-exception in the style guide?

[Alex Meiburg]

There was enough instances of "nonzero" in Mathlib that I was genuinely not sure what the standard was...

[Yaël Dillies]

Yeah, let's not complicate the naming convention but simply fix the names in mathlib