English
In a UFD A, if x ∈ K is integral over A, then x is integral over A in the sense of integers; i.e., IsIntegral A x → IsInteger A x.
Русский
В UFD A, если x ∈ K интегрирован над A, то x является целым числом относительно A; IsIntegral A x → IsInteger A x.
LaTeX
$$$\\text{IsIntegral } A x \\rightarrow \\text{IsInteger } A x$$$
Lean4
theorem exists_integer_of_is_root_of_monic {p : A[X]} (hp : Monic p) {r : K} (hr : aeval r p = 0) :
∃ r' : A, r = algebraMap A K r' ∧ r' ∣ p.coeff 0 := by
/- I tried deducing this from above by unwrapping IsInteger,
but the divisibility condition is annoying -/
obtain ⟨inv, h_inv⟩ := hp ▸ den_dvd_of_is_root hr
use num A r * inv, ?_
· have h : inv ∣ 1 := ⟨den A r, by simpa [mul_comm] using h_inv⟩
simpa using mul_dvd_mul (num_dvd_of_is_root hr) h
· have d_ne_zero : algebraMap A K (den A r) ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (den A r).prop
nth_rw 1 [← mk'_num_den' A r]
rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv), ← map_mul, ← h_inv, map_one, mul_one]
