Def Localization.Away

Modification history

2024-08-09 14:59

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

perf: `to_additive (attr := reducible)` -> `abbrev` (#15476)

Deleted Localization.Away View on Github →

2023-01-30 10:29

Mathlib/GroupTheory/MonoidLocalization.lean

feat: port GroupTheory.Monoid.Localization (#1777)

Added Localization.Away View on Github →