Theorem Localization.mk_one

Modification history

2024-07-03 02:57
Mathlib/GroupTheory/MonoidLocalization.lean
chore(GroupTheory/MonoidLocalization): Change `Localization` to an abbrev of `OreLocalization`. (#13943)
Modified Localization.mk_oneView on Github →
2023-04-12 19:26
Mathlib/GroupTheory/MonoidLocalization.lean
feat: irreducible_def: support protected, equation lemmas (#3395)
Modified Localization.mk_oneView on Github →
2023-01-30 10:29
Mathlib/GroupTheory/MonoidLocalization.lean
feat: port GroupTheory.Monoid.Localization (#1777)
Added Localization.mk_oneView on Github →