Theorem IsLocalization.localization_localization_eq_iff_exists

Modification history

2023-11-16 07:03
Mathlib/RingTheory/Localization/LocalizationLocalization.lean
chore: replace IsLocalization.eq_iff_exists' by exists_of_eq (#8335) …
Deleted IsLocalization.localization_localization_eq_iff_existsView on Github →
2023-05-22 03:13
Mathlib/RingTheory/Localization/LocalizationLocalization.lean
feat: port RingTheory.Localization.LocalizationLocalization (#4137)
Added IsLocalization.localization_localization_eq_iff_existsView on Github →