English
Let A be a UFD and K its fraction field. If x ∈ K is integral over A, then x is an integer over A, i.e., IsIntegral A x implies IsInteger A x.
Русский
Пусть A — UFD и K — его поле дробей. Если x ∈ K интегрирован над A, то x на самом деле целое число относительно A.
LaTeX
$$IsIntegral A x → IsInteger A x$$
Lean4
/-- Rational root theorem part 2:
if `r : f.codomain` is a root of a polynomial over the ufd `A`,
then the denominator of `r` divides the leading coefficient -/
theorem den_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) : (den A r : A) ∣ p.leadingCoeff :=
by
suffices (den A r : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
by
refine dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) ?_ this
intro q dvd_den dvd_num_pow hq
apply hq.not_unit
exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den
rw [← coeff_scaleRoots_natDegree]
apply dvd_term_of_isRoot_of_dvd_terms _ (num_isRoot_scaleRoots_of_aeval_eq_zero hr)
intro j hj
by_cases h : j < p.natDegree
· rw [coeff_scaleRoots]
refine (dvd_mul_of_dvd_right ?_ _).mul_right _
convert pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))
· exact (pow_one _).symm
simpa using h
rw [← natDegree_scaleRoots p (den A r)] at *
rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne (le_of_not_gt h) hj.symm), zero_mul]
exact dvd_zero _
