Theorems · Theorem · commutative algebra

Ideal.mem_map_C_iff

∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} {f : Polynomial R},
  f ∈ Ideal.map Polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I

The push-forward of an ideal I of R to R[X] via inclusion is exactly the set of polynomials whose coefficients are in I

Defined in

Mathlib.RingTheory.Polynomial.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiring