English
Let p ∈ R[X], f: R →+* S be a ring homomorphism, and x ∈ S with p.eval₂ f x = 0. Then the product f(p.leadingCoeff) · x is integral over R.
Русский
Пусть p ∈ R[X], f: R →+* S — кольцевой гомоморфизм, и x ∈ S так, что p.eval₂ f x = 0. Тогда произведение f(p.leadingCoeff) · x является интегральным над R.
LaTeX
$$$\bigl(p.eval_{{f}}(x)=0\bigr) \implies \ IsIntegral_R\Bigl( f(p_{\text{leadingCoeff}}) \cdot x \Bigr)$$$
Lean4
/-- Given a `p : R[X]` and a `x : S` such that `p.eval₂ f x = 0`,
`f p.leadingCoeff * x` is integral. -/
theorem isIntegralElem_leadingCoeff_mul (h : p.eval₂ f x = 0) : f.IsIntegralElem (f p.leadingCoeff * x) :=
by
by_cases h' : 1 ≤ p.natDegree
· use integralNormalization p
have : p ≠ 0 := fun h'' => by
rw [h'', natDegree_zero] at h'
exact Nat.not_succ_le_zero 0 h'
use monic_integralNormalization this
rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]
· by_cases hp : p.map f = 0
· apply_fun fun q => coeff q p.natDegree at hp
rw [coeff_map, coeff_zero, coeff_natDegree] at hp
rw [hp, zero_mul]
exact f.isIntegralElem_zero
· rw [Nat.one_le_iff_ne_zero, Classical.not_not] at h'
rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h
suffices p.map f = 0 by exact (hp this).elim
rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]
