English
In an integrally closed domain R, if p and q are monic polynomials in R[X], and p.map(algebraMap R K) divides q.map(algebraMap R K) in the polynomial ring over K, then q divides p in R[X].
Русский
В интегрально замкнутом домене R, если p и q — моноические многочлены в R[X], и p.map(algebraMap R K) делит q.map(algebraMap R K) в R[X], то q делит p в R[X].
LaTeX
$$$[IsIntegrallyClosed R] \\Rightarrow (p.Monic \\to q.Monic) \\land (q.map(\\mathrm{algebraMap } R K) \\mid p.map(\\mathrm{algebraMap } R K)) \\Rightarrow q \\mid p$$$
Lean4
theorem dvd_of_fraction_map_dvd_fraction_map [IsIntegrallyClosed R] {p q : R[X]} (hp : p.Monic) (hq : q.Monic)
(h : q.map (algebraMap R K) ∣ p.map (algebraMap R K)) : q ∣ p :=
by
obtain ⟨r, hr⟩ := h
obtain ⟨d', hr'⟩ := IsIntegrallyClosed.eq_map_mul_C_of_dvd K hp (dvd_of_mul_left_eq _ hr.symm)
rw [Monic.leadingCoeff, C_1, mul_one] at hr'
· rw [← hr', ← Polynomial.map_mul] at hr
exact dvd_of_mul_right_eq _ (Polynomial.map_injective _ (IsFractionRing.injective R K) hr.symm)
· exact Monic.of_mul_monic_left (hq.map (algebraMap R K)) (by simpa [← hr] using hp.map _)
