Theorems · Definition · commutative algebra

Ideal.polynomialQuotientEquivQuotientPolynomial

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

If I is an ideal of R, then the ring polynomials over the quotient ring I.quotient is isomorphic to the quotient of R[X] by the ideal map C I, where map C I contains exactly the polynomials whose coefficients all lie in I.

Defined in

Mathlib.RingTheory.Polynomial.Quotient

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRing