English
If W(a,b) ≠ 0, then natDegree(W(a,b)) < natDegree(a) + natDegree(b).
Русский
Если W(a,b) ≠ 0, то natDegree(W(a,b)) < natDegree(a) + natDegree(b).
LaTeX
$$$$ \\operatorname{natDegree}( \\mathrm{wronskian}(a,b) ) < a.natDegree + b.natDegree, \\quad \\mathrm{wronskian}(a,b) \\neq 0. $$$$
Lean4
/-- `natDegree` version of the above theorem.
Note this would be false with just `(ha : a ≠ 0) (hb : b ≠ 0),
as when `a = b = 1` we have `(wronskian a b).natDegree = a.natDegree = b.natDegree = 0`.
-/
theorem natDegree_wronskian_lt_add {a b : R[X]} (hw : wronskian a b ≠ 0) :
(wronskian a b).natDegree < a.natDegree + b.natDegree :=
by
have ha : a ≠ 0 := by intro h; subst h; rw [wronskian_zero_left] at hw; exact hw rfl
have hb : b ≠ 0 := by intro h; subst h; rw [wronskian_zero_right] at hw; exact hw rfl
rw [← WithBot.coe_lt_coe, WithBot.coe_add]
convert ← degree_wronskian_lt_add ha hb
· exact Polynomial.degree_eq_natDegree hw
· exact Polynomial.degree_eq_natDegree ha
· exact Polynomial.degree_eq_natDegree hb
