English
If a,b are nonzero polynomials, then the degree of the Wronskian W(a,b) is strictly less than deg(a) + deg(b).
Русский
Если a, b не нули, то deg W(a,b) < deg(a) + deg(b).
LaTeX
$$$$ \\deg( \\mathrm{wronskian}(a,b) ) < \\deg(a) + \\deg(b), \\quad a,b \\neq 0. $$$$
Lean4
/-- Degree of `W(a,b)` is strictly less than the sum of degrees of `a` and `b` (both nonzero). -/
theorem degree_wronskian_lt_add {a b : R[X]} (ha : a ≠ 0) (hb : b ≠ 0) : (wronskian a b).degree < a.degree + b.degree :=
by
calc
(wronskian a b).degree ≤ max (a * derivative b).degree (derivative a * b).degree := Polynomial.degree_sub_le _ _
_ < a.degree + b.degree := by
rw [max_lt_iff]
constructor
case left =>
apply lt_of_le_of_lt
· exact degree_mul_le a (derivative b)
· rw [← Polynomial.degree_ne_bot] at ha
rw [WithBot.add_lt_add_iff_left ha]
exact Polynomial.degree_derivative_lt hb
case right =>
apply lt_of_le_of_lt
· exact degree_mul_le (derivative a) b
· rw [← Polynomial.degree_ne_bot] at hb
rw [WithBot.add_lt_add_iff_right hb]
exact Polynomial.degree_derivative_lt ha
