Theorems · Definition · commutative algebra

AdjoinRoot.quotEquivQuotMap

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

Promote AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot to an AlgEquiv.

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRing