one_inv and inv_one

Stream: general

[Sebastien Gouezel]

docs#one_inv says that 1⁻¹ = 1. And docs#inv_one says that 1⁻¹ = 1. The difference is that one is true in groups, the other one in groups with zeros. What about using inv_one and group_with_zero.inv_one instead?

[Sebastien Gouezel]

Or inv_one and inv_one', maybe?

[Sebastien Gouezel]

Or maybe add two axioms to div_inv_monoid, namely 1⁻¹ = 1 and x⁻¹⁻¹ = x, and use these to treat both situations uniformly (and it would also apply for instance to ennreal). These questions come to my mind while doing the int-smul refactor. I think I'll keep it minimal for now, but there is definitely room for improvement here.

[Eric Wieser]

I think there's some confusion generally about how to apply the naming scheme in the face of projections and notation - 1⁻¹ is either one \inv or inv one depending on whether you write it with notation or not.

Similarly, lemmas about projections are sometimes stated foo.baz_bar (f : foo) : foo.baz (foo.bar f) = _ and sometimes stated foo.bar_baz (f : foo) : f.bar.baz = _. I think we ought to clarify the #naming guide about this