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 {Polynomial.C (Polynomial.X - Polynomial.C a), Polynomial.X - Polynomial.C b} ↔ Polynomial.eval a (Polynomial.eval b P) = 0

theorem Polynomial.ker_evalRingHom {R : Type u_1} [CommRing R] (x : R) : RingHom.ker (Polynomial.evalRingHom x) = Ideal.span {Polynomial.X - Polynomial.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})

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