mathlib

6351f01d - chore(algebra/group_with_zero): cleanup (#5762)

chore(algebra/group_with_zero): cleanup (#5762) * remove `classical,` from proofs: we have `open_locale classical` anyway; * add a lemma `a / (a * a) = a⁻¹`, use it to golf some proofs in other files.