Theorem Submonoid.LocalizationMap.mul_mk'_one_eq_mk'

Modification history

2025-08-13 18:44

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

refactor: make use of `FunLike` for `Submonoid.LocalizationMap` (#22655) …

Modified Submonoid.LocalizationMap.mul_mk'_one_eq_mk'View on Github →

2023-01-30 10:29

Mathlib/GroupTheory/MonoidLocalization.lean

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

Added Submonoid.LocalizationMap.mul_mk'_one_eq_mk'View on Github →