English
For nonzero polynomials p1,p2,q1,q2 with p1 q2 = p2 q1, the integer differences of natural degrees satisfy natDegree(p1) − natDegree(q1) = natDegree(p2) − natDegree(q2).
Русский
Пусть p1,p2,q1,q2 ∈ R[X], все ненулевые, и p1 q2 = p2 q1. Тогда разности натуральных степеней равны: natDegree(p1) − natDegree(q1) = natDegree(p2) − natDegree(q2).
LaTeX
$$$\\\\forall R [\\\\text{Semiring } R] [NoZeroDivisors R], \\\\forall p_1,p_2,q_1,q_2 \\in R[X], \\\\bigl(p_1 \\cdot q_2 = p_2 \\cdot q_1\\\\bigr) \\\\land \\\\, p_1 \\neq 0 \\\\land \\\\, q_1 \\neq 0 \\\\land \\\\, p_2 \\neq 0 \\\\land \\\\, q_2 \\neq 0 \\\\Rightarrow \\\\bigl(p_1.natDegree - q_1.natDegree = p_2.natDegree - q_2.natDegree\\\\)$$$$
Lean4
theorem not_dvd_of_natDegree_lt (h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) : ¬p ∣ q :=
by
by_contra hcontra
exact h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)
