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
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