mathlib

a590d4b5 - feat(group_theory/monoid_localization): some homs induced on localizations: lift, map (#2118)

feat(group_theory/monoid_localization): some homs induced on localizations: lift, map (#2118) * 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 * 2nd section * docs and linting * removing questionable `@[simp]s` * removing away * adding lemmas, removing 'include' * removing import * responding to PR comments * use eq_of_eq to prove comp_eq_of_eq * name change * trying to update mathlib * make lemma names consistent * Update src/algebra/group/is_unit.lean * Update src/algebra/group/is_unit.lean * fix build * documentation and minor changes * spacing * fix build * applying comments Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>