Commit 2025-12-13 22:17 1825e179

View on Github →

chore(Trace/Quotient): move isomorphism to Localization.AtPrime.Basic (#32045) This PR move isomorphisms previously defined in Trace.Quotient into Localization.AtPrime.Basic. The change is purely organizational: Localization.AtPrime.Basic is the canonical place for lemmas and constructions about localization at a prime. The isomorphisms are also renamed to match their new namespace:

equivQuotMaximalIdealOfIsLocalization -> IsLocalization.AtPrime.equivQuotMaximalIdeal
quotMapEquivQuotMapMaximalIdealOfIsLocalization -> IsLocalization.AtPrime.equivQuotMapMaximalIdeal

Estimated changes

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

added theorem IsLocalization.AtPrime.comap_map_eq_map

added def IsLocalization.AtPrime.equivQuotMaximalIdeal

Modified Mathlib/RingTheory/Trace/Quotient.lean

deleted theorem comap_map_eq_map_of_isLocalization_algebraMapSubmonoid

deleted def equivQuotMaximalIdealOfIsLocalization

deleted def quotMapEquivQuotMapMaximalIdealOfIsLocalization