mathlib
3ea573ef - refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids (#14042)

Commit
3 years ago
refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids (#14042) Delete the `group` and `group_with_zero` lemmas which have been made one-liners in #14000. 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 Lemma renames
Author
Parents
Loading