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) : q.modByMonicHom.ker = 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_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (I : Ideal R) {y : ↥R[x]} : y ∈ Ideal.map (algebraMap R ↥R[x]) I ↔ ∃ (p : Polynomial R), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (Polynomial.aeval x) p = ↑y

theorem Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) (I : Ideal R) (hI : I ≠ ⊤) [Invertible x] (h : Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤) : ∃ (p : Polynomial R), p.leadingCoeff - 1 ∈ I ∧ (Polynomial.aeval ⅟x) p = 0