Theorems · Definition · commutative algebra

AdjoinRoot.Polynomial.quotQuotEquivComm

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

The natural isomorphism (R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x]) where f : R[X] and I : Ideal R

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRing