mathlib3
bf6e13bf - refactor(algebra/{group,group_with_zero/basic): Generalize lemmas to division monoids (#14000)

Commit
3 years ago
refactor(algebra/{group,group_with_zero/basic): Generalize lemmas to division monoids (#14000) Generalize `group` and `group_with_zero` lemmas to `division_monoid`. We do not actually delete the original lemmas but make them one-liners from the new ones. The next PR will then delete the old lemmas and perform the renames in all files. Lemmas are renamed because * one of the `group` or `group_with_zero` name has to go * the new API should have a consistent naming convention Pre-emptive lemma renames
Author
Parents
Loading