English
For nonzero polynomials p1,p2,q1,q2 with p1*q2 = p2*q1, the equality of degree differences holds; equivalently, the top-degree differences are preserved under cross-multiplication.
Русский
Для ненулевых полиномов p1,p2,q1,q2 при p1 q2 = p2 q1 выполняется равенство разностей степеней: p1.natDegree - q1.natDegree = p2.natDegree - q2.natDegree.
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) \\\\Rightarrow \\\\left(p_1.natDegree - q_1.natDegree = p_2.natDegree - q_2.natDegree\\right)$$$
Lean4
/-- This lemma is useful for working with the `intDegree` of a rational function. -/
theorem natDegree_sub_eq_of_prod_eq {p₁ p₂ q₁ q₂ : R[X]} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0) (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0)
(h_eq : p₁ * q₂ = p₂ * q₁) : (p₁.natDegree : ℤ) - q₁.natDegree = (p₂.natDegree : ℤ) - q₂.natDegree :=
by
rw [sub_eq_sub_iff_add_eq_add]
norm_cast
rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]
