English
There exists a primitive polynomial r such that for every polynomial s, p ∣ s and q ∣ s if and only if r ∣ s.
Русский
Существует примитивный многочлен r, такой что для любого s выполняется p ∣ s и q ∣ s тогда и только тогда r ∣ s.
LaTeX
$$$\exists r \in R[X], r.IsPrimitive \land \forall s:\ R[X], (p \mid s \land q \mid s) \iff r \mid s$$$
Lean4
theorem exists_primitive_lcm_of_isPrimitive {p q : R[X]} (hp : p.IsPrimitive) (hq : q.IsPrimitive) :
∃ r : R[X], r.IsPrimitive ∧ ∀ s : R[X], p ∣ s ∧ q ∣ s ↔ r ∣ s := by
classical
have h : ∃ (n : ℕ) (r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r :=
⟨(p * q).natDegree, p * q, rfl, hp.mul hq, dvd_mul_right _ _, dvd_mul_left _ _⟩
rcases Nat.find_spec h with ⟨r, rdeg, rprim, pr, qr⟩
refine ⟨r, rprim, fun s => ⟨?_, fun rs => ⟨pr.trans rs, qr.trans rs⟩⟩⟩
suffices hs : ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s from hs s.natDegree s rfl
clear s
by_contra! con
rcases Nat.find_spec con with ⟨s, sdeg, ⟨ps, qs⟩, rs⟩
have s0 : s ≠ 0 := by
contrapose! rs
simp [rs]
have hs :=
Nat.find_min' h
⟨_, s.natDegree_primPart, s.isPrimitive_primPart, (hp.dvd_primPart_iff_dvd s0).2 ps,
(hq.dvd_primPart_iff_dvd s0).2 qs⟩
rw [← rdeg] at hs
by_cases sC : s.natDegree ≤ 0
· rw [eq_C_of_natDegree_le_zero (le_trans hs sC), isPrimitive_iff_content_eq_one, content_C,
normalize_eq_one] at rprim
rw [eq_C_of_natDegree_le_zero (le_trans hs sC), ← dvd_content_iff_C_dvd] at rs
apply rs rprim.dvd
have hcancel := natDegree_cancelLeads_lt_of_natDegree_le_natDegree hs (lt_of_not_ge sC)
rw [sdeg] at hcancel
apply Nat.find_min con hcancel
refine ⟨_, rfl, ⟨dvd_cancelLeads_of_dvd_of_dvd pr ps, dvd_cancelLeads_of_dvd_of_dvd qr qs⟩, fun rcs => rs ?_⟩
rw [← rprim.dvd_primPart_iff_dvd s0]
rw [cancelLeads, tsub_eq_zero_iff_le.mpr hs, pow_zero, mul_one] at rcs
have h := dvd_add rcs (Dvd.intro_left (C (leadingCoeff s) * X ^ (natDegree s - natDegree r)) rfl)
have hC0 := rprim.ne_zero
rw [Ne, ← leadingCoeff_eq_zero, ← C_eq_zero] at hC0
rw [sub_add_cancel, ← rprim.dvd_primPart_iff_dvd (mul_ne_zero hC0 s0)] at h
rcases isUnit_primPart_C r.leadingCoeff with ⟨u, hu⟩
apply h.trans (Associated.symm ⟨u, _⟩).dvd
rw [primPart_mul (mul_ne_zero hC0 s0), hu, mul_comm]
