Theorem Submonoid.LocalizationMap.lift_localizationMap_mk'

Modification history

2026-02-04 10:57
Mathlib/GroupTheory/MonoidLocalization/Basic.lean
refactor(GroupTheory/MonoidLocalization): split long file (#34811) …
Modified Submonoid.LocalizationMap.lift_localizationMap_mk'View on Github →
2025-03-24 18:17
Mathlib/GroupTheory/MonoidLocalization/Basic.lean
refactor(GroupTheory/MonoidLocalization): tweak `simp`-normal form (#23263) …
Added Submonoid.LocalizationMap.lift_localizationMap_mk'View on Github →