mathlib
737784ef - refactor(algebra/{group_power/{basic,lemmas},group_with_zero/power}): Generalize lemmas to division monoids (#14102)

Commit
3 years ago
refactor(algebra/{group_power/{basic,lemmas},group_with_zero/power}): Generalize lemmas to division monoids (#14102) Generalize `group` and `group_with_zero` lemmas about `zpow` to `division_monoid`. Lemmas are renamed because one of the `group` or `group_with_zero` name has to go. It's just a matter of removing the suffixed `₀`. Lemma renames
Author
Parents
Loading