Radical of a polynomial

This file proves some theorems on radical and divRadical of polynomials. See RingTheory.Radical for the definition of radical and divRadical.

theorem degree_radical_le {k : Type u_1} [Field k] [DecidableEq k] {a : Polynomial k} (h : a ≠ 0) : (UniqueFactorizationMonoid.radical a).degree ≤ a.degree

theorem natDegree_radical_le {k : Type u_1} [Field k] [DecidableEq k] {a : Polynomial k} : (UniqueFactorizationMonoid.radical a).natDegree ≤ a.natDegree

theorem divRadical_dvd_derivative {k : Type u_1} [Field k] [DecidableEq k] (a : Polynomial k) : EuclideanDomain.divRadical a ∣ Polynomial.derivative a

theorem divRadical_dvd_wronskian_left {k : Type u_1} [Field k] [DecidableEq k] (a b : Polynomial k) : EuclideanDomain.divRadical a ∣ a.wronskian b

theorem divRadical_dvd_wronskian_right {k : Type u_1} [Field k] [DecidableEq k] (a b : Polynomial k) : EuclideanDomain.divRadical b ∣ a.wronskian b