LeanPool.LeanPolyABC.Lib.Wronskian

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

Wronskian: W(a, b) = ab' - a'b.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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