Theorems · Theorem · commutative algebra

AdjoinRoot.quotEquivQuotMap_symm_apply

∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (I : Ideal R)
  (a : Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}),
  (AdjoinRoot.quotEquivQuotMap f I).symm a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f).symm a

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing