mathlib
649ca66b - chore(*): Disparate generalizations to division monoids (#14686)

Commit

3 years ago

chore(*): Disparate generalizations to division monoids (#14686) The leftover changes from the introduction of `division_monoid`.

Author

YaelDillies

Parents