divRadical_dvd_wronskian_left — Mathlib

English

For any polynomials a,b over k, the radical of a divides the Wronskian of a and b.

Русский

Пусть a,b — многочлены над k. Тогда радикал(a) делитWronskian(a,b).

LaTeX

$$$\\operatorname{divRadical}(a) \\mid \\operatorname{wronskian}(a,b)$$$

Lean4

theorem divRadical_dvd_wronskian_left (a b : k[X]) : divRadical a ∣ wronskian a b :=
  by
  rw [wronskian]
  apply dvd_sub
  · apply dvd_mul_of_dvd_left
    exact divRadical_dvd_self a
  · apply dvd_mul_of_dvd_left
    exact divRadical_dvd_derivative a

Похожие утверждения