Theorems · Theorem · commutative algebra

AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk

∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
      ((DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p) =
    (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I)))
      ((AdjoinRoot.mk f) p)

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing