postfix lemma naming for inv

Stream: general

[Yakov Pechersky]

In #11617, Johan asked me to rename inv_one to one_inv and friends, like inv_X to X_inv. I couldn't find the convention on https://leanprover-community.github.io/contribute/naming.html. I did an analysis on master and found inv_* more than *_inv:

(base) ➜  mathlib git:(master) ✗ rg -w zero_inv | rg lemma
(base) ➜  mathlib git:(master) ✗ rg -w inv_zero | rg lemma
src/algebra/group/with_one.lean:@[simp] lemma inv_zero [has_inv α] :
src/ring_theory/dedekind_domain.lean:lemma inv_zero' : (0 : fractional_ideal R₁⁰ K)⁻¹ = 0 := fractional_ideal.div_zero
src/algebra/group_with_zero/defs.lean:@[simp] lemma inv_zero : (0 : G₀)⁻¹ = 0 :=
src/linear_algebra/matrix/nonsingular_inverse.lean:@[simp] lemma inv_zero : (0 : matrix n n α)⁻¹ = 0 :=
src/data/real/ennreal.lean:@[simp] lemma inv_zero : (0 : ℝ≥0∞)⁻¹ = ∞ :=
src/data/complex/basic.lean:protected lemma inv_zero : (0⁻¹ : ℂ) = 0 :=
src/data/zmod/basic.lean:lemma inv_zero : ∀ (n : ℕ), (0 : zmod n)⁻¹ = 0
src/data/complex/is_R_or_C.lean:protected lemma inv_zero : (0⁻¹ : K) = 0 :=

for token in one zero smul; do echo $token; rg -w inv_${token} | rg "(lemma|theorem)" -c; rg -w ${token}_inv | rg "(lemma|theorem)" -c || echo 0; done
one
5
4
zero
9
0
smul
3
5

[Yakov Pechersky]

/poll Naming of lemmas for postfix operators
Always before inv_one transpose_one
Always after one_inv one_transpose
After only in the case of inv, arbitrary elsewhere one_inv, transpose_one
Arbitrary everywhere

[Yakov Pechersky]

I did change the PR according to the reviewer, thus making the only zero_inv lemmas in mathlib. But I do prefer inv_zero because, without notation, that is the underlying expression.

[Eric Rodriguez]

<deleted: it did work after refresh>

[Yaël Dillies]

Similarly, we have compl which I think should be prefix.

[Floris van Doorn]

If it has (postfix) notation or localized notation, I think we should follow the order specified by the notation.

[Floris van Doorn]

That is also the motivation behind names like zero_add and add_zero: those names only make sense if add is infix.

[Floris van Doorn]

Aside: when something is written with projection notation I think it should also be after, but that is trickier, since projection notation is more voluntary.
If something is not written with notation I think it should always come before (injective_foo, not foo_injective), but I think I've been outvoted about that before.

[Eric Wieser]

foo_injective is specifically advocated by #naming

[Yury G. Kudryashov]

It was added to #naming after a vote somewhere here.