LeanPool.LeanPolyABC.Lib.DivRadical

noncomputable def LeanPolyABC.Polynomial.divRadical {k : Type u_1} [Field k] [DecidableEq k] (a : Polynomial k) : Polynomial k

For a given polynomial a, a.divRadical is a divided by its radical radical a. This is the key to our implementation.

Equations

• LeanPolyABC.Polynomial.divRadical a = a / LeanPolyABC.radical a

theorem LeanPolyABC.Polynomial.hMul_radical_divRadical {k : Type u_1} [Field k] [DecidableEq k] (a : Polynomial k) : radical a * divRadical a = a

theorem LeanPolyABC.Polynomial.divRadical_ne_zero {k : Type u_1} [Field k] [DecidableEq k] {a : Polynomial k} (ha : a ≠ 0) : divRadical a ≠ 0

theorem LeanPolyABC.Polynomial.divRadical_isUnit {k : Type u_1} [Field k] [DecidableEq k] {u : Polynomial k} (hu : IsUnit u) : IsUnit (divRadical u)

theorem LeanPolyABC.Polynomial.eq_divRadical {k : Type u_1} [Field k] [DecidableEq k] {a x : Polynomial k} (h : radical a * x = a) : x = divRadical a

theorem LeanPolyABC.Polynomial.divRadical_hMul {k : Type u_1} [Field k] [DecidableEq k] {a b : Polynomial k} (hc : IsCoprime a b) : divRadical (a * b) = divRadical a * divRadical b

theorem LeanPolyABC.Polynomial.divRadical_dvd_self {k : Type u_1} [Field k] [DecidableEq k] (a : Polynomial k) : divRadical a ∣ a

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

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

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