units): Units in division monoids (#14212)

Commit

3 years ago

feat(algebra/{group,hom}/units): Units in division monoids (#14212) Copy over `group_with_zero` lemmas to the more general setting of `division_monoid`.

Author

YaelDillies

Parents

050404af

mathlib 13b999c4 - feat(algebra/{group,hom}/units): Units in division monoids (#14212)

mathlib
13b999c4 - feat(algebra/{group,hom}/units): Units in division monoids (#14212)