Ideals in polynomial rings

theorem Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero {R : Type u_1} [CommRing R] {a : R} {b : Polynomial R} {P : Polynomial (Polynomial R)} : P ∈ Ideal.span {C (X - C a), X - C b} ↔ eval a (eval b P) = 0

theorem Polynomial.ker_evalRingHom {R : Type u_1} [CommRing R] (x : R) : RingHom.ker (evalRingHom x) = Ideal.span {X - C x}

@[simp]

theorem Polynomial.ker_modByMonicHom {R : Type u_1} [CommRing R] {q : Polynomial R} (hq : q.Monic) : LinearMap.ker q.modByMonicHom = Submodule.restrictScalars R (Ideal.span {q})

@[simp]

theorem Polynomial.ker_constantCoeff {R : Type u_1} [CommRing R] : RingHom.ker constantCoeff = Ideal.span {X}

theorem Algebra.mem_ideal_map_adjoin {R : Type u_2} {S : Type u_3} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (I : Ideal R) {y : ↥(adjoin R {x})} : y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I ↔ ∃ (p : Polynomial R), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (Polynomial.aeval x) p = ↑y