Theorems · Definition · commutative algebra

Polynomial.quotientSpanXSubCAlgEquiv

{R : Type u_1} → [inst : CommRing R] → (x : R) → (Polynomial R ⧸ Ideal.span {Polynomial.X - Polynomial.C x}) ≃ₐ[R] R

For a commutative ring $R$, evaluating a polynomial at an element $x \in R$ induces an isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$.

Defined in

Mathlib.RingTheory.Polynomial.Quotient

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRing