English
For coprime polynomials a,b over NoZeroDivisors, we have W(a,b) = 0 iff derivatives are zero: derivative a = 0 and derivative b = 0.
Русский
Для взаимно простых многочленов a,b над кольцом без нулевых делителей, W(a,b) = 0 тогда и только тогда, когда производные равны нулю: a' = 0 и b' = 0.
LaTeX
$$$$ \\text{If } \\mathrm{IsCoprime}(a,b) \\text{ then } \\mathrm{wronskian}(a,b) = 0 \\iff \\big( \\mathrm{derivative}(a) = 0 \\land \\mathrm{derivative}(b) = 0 \\big). $$$$
Lean4
/-- For coprime polynomials `a` and `b`, their Wronskian is zero
if and only if their derivatives are zeros.
-/
theorem _root_.IsCoprime.wronskian_eq_zero_iff [NoZeroDivisors R] {a b : R[X]} (hc : IsCoprime a b) :
wronskian a b = 0 ↔ derivative a = 0 ∧ derivative b = 0
where
mp
hw := by
rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw
constructor
· rw [← dvd_derivative_iff]
apply hc.dvd_of_dvd_mul_right
rw [← hw]; exact dvd_mul_right _ _
· rw [← dvd_derivative_iff]
apply hc.symm.dvd_of_dvd_mul_left
rw [hw]; exact dvd_mul_left _ _
mpr
hdab := by
obtain ⟨hda, hdb⟩ := hdab
rw [wronskian]
rw [hda, hdb]; simp only [mul_zero, zero_mul, sub_self]
