Theorem Submonoid.LocalizationWithZeroMap.lift_def

Modification history

2025-08-22 15:03
Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
chore(MonoidLocalization): get rid of Submonoid.LocalizationWithZeroMap (#27842) …
Deleted Submonoid.LocalizationWithZeroMap.lift_defView on Github →
2025-03-30 21:32
Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
refactor(RingTheory): small `erw`-removing refactors to localizations (#23375) …
Added Submonoid.LocalizationWithZeroMap.lift_defView on Github →