English
If an ideal I of S[X] contains a monic polynomial g, then the image of X in the quotient S[X]/I is integral over S.
Русский
Если идеал I в S[X] содержит моноический многочлен g, то образ X в факторкольце S[X]/I интегрален над S.
LaTeX
$$$g\in I\text{ and } g\text{ is Monic }\Rightarrow ((\operatorname{Ideal.Quotient.mk} I)\circ (\text{algebraMap } S S[X])).IsIntegralElem (\operatorname{Ideal.Quotient.mk} I X)$$$
Lean4
theorem quotient_isIntegralElem {g : S[X]} (mon : g.Monic) {I : Ideal S[X]} (h : g ∈ I) :
((Ideal.Quotient.mk I).comp (algebraMap S S[X])).IsIntegralElem (Ideal.Quotient.mk I X) := by
exact
⟨g, mon, by
rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]
nth_rw 3 [(as_sum_range_C_mul_X_pow g)]
simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]⟩
/- If `I` is an ideal of the polynomial ring `S[X]` and contains a monic polynomial `f`,
then `S[X]/I` is integral over `S`. -/
