mathlib

4f10d1eb - refactor(group_theory/monoid_localization): use characteristic predicate (#2004)

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 Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>