Commit 2026-05-05 14:28 4218a646

View on Github →

feat(RingTheory/Localization): R ⧸ pⁿ ≃ₐ[R] Rₚ ⧸ (maximalIdeal Rₚ)ⁿ (#36783) This extends the existing def equivQuotMaximalIdeal : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ to powers of maximal ideals.

Estimated changes

Modified Mathlib/Algebra/Group/Units/Hom.lean

added theorem IsUnit.liftRight_apply

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

added theorem RingEquiv.coe_subringCongr_apply

added theorem RingEquiv.subringCongr_symm

Modified Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean

added theorem Ideal.Quotient.isUnit_mk_pow_of_notMem

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

added theorem IsLocalization.AtPrime.comap_maximalIdeal_pow

added def IsLocalization.AtPrime.equivQuotMaximalIdealPow

added theorem IsLocalization.AtPrime.equivQuotMaximalIdealPow_apply_mk

added theorem IsLocalization.AtPrime.equivQuotMaximalIdealPow_symm_apply_mk_mul