Wronskian of a pair of polynomial

This file defines Wronskian of a pair of polynomials, which is W(a, b) = ab' - a'b. We also prove basic properties of it.

Main declarations

• Polynomial.wronskian_eq_of_sum_zero: We have W(a, b) = W(b, c) when a + b + c = 0.
• Polynomial.degree_wronskian_lt_add: Degree of Wronskian W(a, b) is strictly smaller than the sum of degrees of a and b
• Polynomial.natDegree_wronskian_lt_add: natDegree version of the above theorem. We need to assume that the Wronskian is nonzero. (Otherwise, a = b = 1 gives a counterexample.)

TODO

• Define Wronskian for n-tuple of polynomials, not necessarily two.

noncomputable def Polynomial.wronskian {R : Type u_1} [CommRing R] (a b : Polynomial R) : Polynomial R

Wronskian of a pair of polynomials, W(a, b) = ab' - a'b.

Equations

• a.wronskian b = a * Polynomial.derivative b - Polynomial.derivative a * b

noncomputable def Polynomial.wronskianBilin (R : Type u_1) [CommRing R] : Polynomial R →ₗ[R] Polynomial R →ₗ[R] Polynomial R

Polynomial.wronskian as a bilinear map.

Equations

• Polynomial.wronskianBilin R = (LinearMap.mul R (Polynomial R)).compl₂ Polynomial.derivative - LinearMap.mul R (Polynomial R) ∘ₗ Polynomial.derivative

@[simp]

theorem Polynomial.wronskianBilin_apply {R : Type u_1} [CommRing R] (a b : Polynomial R) : ((wronskianBilin R) a) b = a.wronskian b

@[simp]

theorem Polynomial.wronskian_zero_left {R : Type u_1} [CommRing R] (a : Polynomial R) : wronskian 0 a = 0

@[simp]

theorem Polynomial.wronskian_zero_right {R : Type u_1} [CommRing R] (a : Polynomial R) : a.wronskian 0 = 0

theorem Polynomial.wronskian_neg_left {R : Type u_1} [CommRing R] (a b : Polynomial R) : (-a).wronskian b = -a.wronskian b

theorem Polynomial.wronskian_neg_right {R : Type u_1} [CommRing R] (a b : Polynomial R) : a.wronskian (-b) = -a.wronskian b

theorem Polynomial.wronskian_add_right {R : Type u_1} [CommRing R] (a b c : Polynomial R) : a.wronskian (b + c) = a.wronskian b + a.wronskian c

theorem Polynomial.wronskian_add_left {R : Type u_1} [CommRing R] (a b c : Polynomial R) : (a + b).wronskian c = a.wronskian c + b.wronskian c

theorem Polynomial.wronskian_self_eq_zero {R : Type u_1} [CommRing R] (a : Polynomial R) : a.wronskian a = 0

theorem Polynomial.isAlt_wronskianBilin {R : Type u_1} [CommRing R] : (wronskianBilin R).IsAlt

theorem Polynomial.wronskian_neg_eq {R : Type u_1} [CommRing R] (a b : Polynomial R) : -a.wronskian b = b.wronskian a

theorem Polynomial.wronskian_eq_of_sum_zero {R : Type u_1} [CommRing R] {a b c : Polynomial R} (hAdd : a + b + c = 0) : a.wronskian b = b.wronskian c

theorem Polynomial.degree_wronskian_lt_add {R : Type u_1} [CommRing R] {a b : Polynomial R} (ha : a ≠ 0) (hb : b ≠ 0) : (a.wronskian b).degree < a.degree + b.degree

Degree of W(a,b) is strictly less than the sum of degrees of a and b (both nonzero).

theorem Polynomial.natDegree_wronskian_lt_add {R : Type u_1} [CommRing R] {a b : Polynomial R} (hw : a.wronskian b ≠ 0) : (a.wronskian b).natDegree < a.natDegree + b.natDegree

natDegree version of the above theorem. Note this would be false with just (ha : a ≠ 0) and (hb : b ≠ 0), since when a = b = 1 we have (wronskian a b).natDegree = a.natDegree = b.natDegree = 0.

theorem IsCoprime.wronskian_eq_zero_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {a b : Polynomial R} (hc : IsCoprime a b) : a.wronskian b = 0 ↔ Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0

For coprime polynomials a and b, their Wronskian is zero if and only if their derivatives are zeros.