Commit 2022-05-09 00:34 bf6e13bf
View on Github →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
orgroup_with_zero
name has to go - the new API should have a consistent naming convention Pre-emptive lemma renames