English
Let p, q be polynomials over a semiring in which p is Monic, p ∣ q, and q.natDegree ≤ p.natDegree. Then q = C(q.leadingCoeff) · p.
Русский
Пусть p, q — многочлены над полем, p моноическая, p делит q, и q.natDegree ≤ p.natDegree. Тогда q = C(q.leadingCoeff) · p.
LaTeX
$$hp : p.Monic, hdiv : p ∣ q, hdeg : q.natDegree ≤ p.natDegree ⟹ q = C(q.leadingCoeff) * p$$
Lean4
theorem eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R} [CommSemiring R] {p q : R[X]} (hp : p.Monic)
(hdiv : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) : q = C q.leadingCoeff * p :=
by
obtain ⟨r, hr⟩ := hdiv
obtain rfl | hq := eq_or_ne q 0; · simp
have rzero : r ≠ 0 := fun h => by simp [h, hq] at hr
rw [hr, natDegree_mul'] at hdeg; swap
· rw [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
exact rzero
rw [mul_comm, @eq_C_of_natDegree_eq_zero _ _ r] at hr
· convert hr
convert leadingCoeff_C (coeff r 0) using 1
rw [hr, leadingCoeff_mul_monic hp]
· exact (add_right_inj _).1 (le_antisymm hdeg <| Nat.le.intro rfl)
