Theorem IsLocalization.localization_localization_exists_of_eq

Modification history

2023-11-16 07:03
Mathlib/RingTheory/Localization/LocalizationLocalization.lean
chore: replace IsLocalization.eq_iff_exists' by exists_of_eq (#8335) …
Added IsLocalization.localization_localization_exists_of_eqView on Github →