Def IsLocalization.toLocalizationWithZeroMap

Modification history

2025-08-22 15:03
Mathlib/RingTheory/Localization/Defs.lean
chore(MonoidLocalization): get rid of Submonoid.LocalizationWithZeroMap (#27842) …
Deleted IsLocalization.toLocalizationWithZeroMapView on Github →
2024-10-15 07:35
Mathlib/RingTheory/Localization/Basic.lean
chore(RingTheory/Localization/Basic): split off `Defs` (#17735) …
Modified IsLocalization.toLocalizationWithZeroMapView on Github →
2023-11-16 07:03
Mathlib/RingTheory/Localization/Basic.lean
chore: replace IsLocalization.eq_iff_exists' by exists_of_eq (#8335) …
Modified IsLocalization.toLocalizationWithZeroMapView on Github →
2023-03-09 14:54
Mathlib/RingTheory/Localization/Basic.lean
feat: port/RingTheory.Localization.Basic (#2741)
Added IsLocalization.toLocalizationWithZeroMapView on Github →