mathlib3

04e2f5f7 - feat(algebra/group/basic): add a few lemmas (#10856)

feat(algebra/group/basic): add a few lemmas (#10856) * move `inv_eq_one`, `one_eq_inv`, and `inv_ne_one` up; * move `div_one'` below `div_eq_one` to golf the proof; * add `div_eq_inv_iff`; * golf 2 proofs.