Commit 2021-12-18 14:23 04e2f5f7
View on Github →feat(algebra/group/basic): add a few lemmas (#10856)
- move
inv_eq_one,one_eq_inv, andinv_ne_oneup; - move
div_one'belowdiv_eq_oneto golf the proof; - add
div_eq_inv_iff; - golf 2 proofs.
feat(algebra/group/basic): add a few lemmas (#10856)
inv_eq_one, one_eq_inv, and inv_ne_one up;div_one' below div_eq_one to golf the proof;div_eq_inv_iff;