Commit 2020-03-06 19:21 4f10d1eb
View on Github →refactor(group_theory/monoid_localization): use characteristic predicate (#2004)
- should I be changing and committing toml idk
- initial monoid loc lemmas
- responding to PR comments
- removing bad @[simp]
- inhabited instances
- remove #lint
- additive inhabited instance
- using is_unit & is_add_unit
- doc string
- remove simp
- submonoid.monoid_loc... -> submonoid.localization
- submonoid.monoid_loc... -> submonoid.localization
- generalize inhabited instance
- remove inhabited instance