Theorems · Theorem · commutative algebra

Ideal.eq_zero_of_polynomial_mem_map_range

∀ {R : Type u_1} [inst : CommRing R] (I : Ideal (Polynomial R)) (x : ↥((Ideal.Quotient.mk I).comp Polynomial.C).range),
  Polynomial.C x ∈ Ideal.map (Polynomial.mapRingHom ((Ideal.Quotient.mk I).comp Polynomial.C).rangeRestrict) I → x = 0

Given any ring R and an ideal I of R[X], we get a map R → R[x] → R[x]/I. If we let R be the image of R in R[x]/I then we also have a map R[x] → R'[x]. In particular we can map I across this map, to get I' and a new map R' → R'[x] → R'[x]/I. This theorem shows I' will not contain any non-zero constant polynomials.

Defined in

Mathlib.RingTheory.Polynomial.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing