Further properties of the Wronskian of two polynomials

This file adds four facts about Mathlib's Wronskian W(a, b) = a b' - a' b of two polynomials: it commutes with coefficient ring maps, it is unchanged when a constant multiple of a is subtracted from b, a root of multiplicity n of b is a root of multiplicity at least n - 1 of W(a, b), and its coefficient in degree 2 deg a is leadingCoeff a · leadingCoeff b when deg b = deg a + 1.

The first three are the steps of Thue's argument that transport vanishing of a polynomial pair at a point to its Wronskian.

Main results

• Polynomial.map_wronskian: W(a, b) commutes with coefficient ring maps.
• Polynomial.wronskian_sub_C_mul_right: W(a, b - c a) = W(a, b) for a constant c.
• Polynomial.pow_sub_one_dvd_wronskian_right: if q ^ n ∣ b, then q ^ (n - 1) ∣ W(a, b).
• Polynomial.coeff_wronskian_of_natDegree_eq_succ: if deg b = deg a + 1, then the coefficient of W(a, b) in degree 2 deg a is leadingCoeff a · leadingCoeff b.

@[simp]

theorem Polynomial.map_wronskian {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (a b : Polynomial R) : map f (a.wronskian b) = (map f a).wronskian (map f b)

The Wronskian commutes with coefficient ring maps.

@[simp]

theorem Polynomial.wronskian_sub_C_mul_right {R : Type u_1} [CommRing R] (a b : Polynomial R) (c : R) : a.wronskian (b - C c * a) = a.wronskian b

The Wronskian W(a, b) does not change when a constant multiple of a is subtracted from b.

theorem Polynomial.pow_sub_one_dvd_wronskian_right {R : Type u_1} [CommRing R] {a b q : Polynomial R} {n : ℕ} (h : q ^ n ∣ b) : q ^ (n - 1) ∣ a.wronskian b

If q ^ n divides b, then q ^ (n - 1) divides the Wronskian W(a, b).

theorem Polynomial.coeff_wronskian_of_natDegree_eq_succ {R : Type u_1} [CommRing R] {a b : Polynomial R} (h : b.natDegree = a.natDegree + 1) : (a.wronskian b).coeff (2 * a.natDegree) = a.leadingCoeff * b.leadingCoeff

If deg b = deg a + 1, then the coefficient of the Wronskian W(a, b) = a b' - a' b in degree 2 deg a is leadingCoeff a · leadingCoeff b: the top terms of a b' and a' b contribute (deg a + 1) and deg a times this product.