Theorems · Theorem · commutative algebra

MvPolynomial.mem_map_C_iff

∀ {R : Type u} {σ : Type v} [inst : CommRing R] {I : Ideal R} {f : MvPolynomial σ R},
  f ∈ Ideal.map MvPolynomial.C I ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m f ∈ I

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

Defined in

Mathlib.RingTheory.Polynomial.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing