English
If p and q are primitive polynomials over R and their images under the fraction-map division are related, then p divides q: more precisely, if p.IsPrimitive and q.IsPrimitive and p.map( algebraMap R K ) divides q.map(algebraMap R K), then p divides q in R[X].
Русский
Если p и q — примитивные полиномы над R и их образы в дробной области связаны делением, то p делит q в R[X].
LaTeX
$$p.IsPrimitive → q.IsPrimitive → (p.map(\\mathrm{algebraMap} R K) ∣ q.map(\\mathrm{algebraMap} R K)) → p ∣ q$$
Lean4
theorem dvd_of_fraction_map_dvd_fraction_map {p q : R[X]} (hp : p.IsPrimitive) (hq : q.IsPrimitive)
(h_dvd : p.map (algebraMap R K) ∣ q.map (algebraMap R K)) : p ∣ q :=
by
rcases h_dvd with ⟨r, hr⟩
obtain ⟨⟨s, s0⟩, hs⟩ := integerNormalization_map_to_map R⁰ r
rw [Subtype.coe_mk, Algebra.smul_def, algebraMap_apply] at hs
have h : p ∣ q * C s := by
use integerNormalization R⁰ r
apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)
rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]
simp
rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h
· exact h
· symm
rcases isUnit_primPart_C s with ⟨u, hu⟩
use u
rw [hu]
iterate 2
apply mul_ne_zero hq.ne_zero
rw [Ne, C_eq_zero]
contrapose! s0
simp [s0, mem_nonZeroDivisors_iff_ne_zero]
