Lemmas for ideal in polynomial span by monic polynomial

theorem Polynomial.exists_monic_span {k : Type u_2} [Field k] (I : Ideal (Polynomial k)) (ne : I ≠ ⊥) : ∃ (f : Polynomial k), f.Monic ∧ I = Ideal.span {f}

theorem Polynomial.exists_monic_span_sup_map_eq (R : Type u_1) [CommRing R] (p : Ideal (Polynomial R)) (ism : (Ideal.comap C p).IsMaximal) (ne : p ≠ Ideal.map C (Ideal.comap C p)) : ∃ (f : Polynomial R), f.Monic ∧ p = Ideal.map C (Ideal.comap C p) ⊔ Ideal.span {f}