Theorems · Definition · commutative algebra

AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk

{R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (f : Polynomial R) →
        AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.mk f) (Ideal.map Polynomial.C I) ≃+*
          (Polynomial R ⧸ Ideal.map Polynomial.C I) ⧸
            Ideal.map (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) (Ideal.span {f})

The natural isomorphism R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x]) for α a root of f : R[X] and I : Ideal R

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRing