Theorem IsLocalization.eq_mk'_of_mul_eq

Modification history

2024-10-15 07:35

Mathlib/RingTheory/Localization/Basic.lean

chore(RingTheory/Localization/Basic): split off `Defs` (#17735) …

Modified IsLocalization.eq_mk'_of_mul_eq View on Github →

2024-09-16 11:07

Mathlib/RingTheory/Localization/Basic.lean

feat(RingTheory/IntegralClosure/IntegrallyClosed): `IsIntegrallyClosed` is a local property (#16558) …

Added IsLocalization.eq_mk'_of_mul_eq View on Github →