Theorems · Definition · commutative algebra

IsLocalization.AtPrime.equivQuotMaximalIdealPow

{R : Type u_7} →
  [inst : CommRing R] →
    (p : Ideal R) →
      [inst_1 : p.IsMaximal] →
        (Rₚ : Type u_8) →
          [inst_2 : CommRing Rₚ] →
            [inst_3 : Algebra R Rₚ] →
              [IsLocalization.AtPrime Rₚ p] →
                [inst_5 : IsLocalRing Rₚ] → (n : ℕ) → (R ⧸ p ^ n) ≃ₐ[R] Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ ^ n

The isomorphism R ⧸ p ^ n ≃ₐ[R] Rₚ ⧸ maximalIdeal Rₚ ^ n, where Rₚ satisfies IsLocalization.AtPrime Rₚ p.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

2 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIdeal.IsMaximalCommRingAlgebraIsLocalization.AtPrimeIsLocalRing