English
For any polynomial a over k, the radical of a divides its derivative a'.
Русский
Для любого многочлена a над k радикал(a) делит производную a'.
LaTeX
$$$\\operatorname{divRadical}(a) \\mid a'.$$$
Lean4
theorem divRadical_dvd_derivative (a : k[X]) : divRadical a ∣ derivative a :=
by
induction a using induction_on_coprime
·
case h0 =>
rw [derivative_zero]
apply dvd_zero
· case h1 a ha => exact (divRadical_isUnit ha).dvd
·
case hpr p i hp =>
cases i
· rw [pow_zero, derivative_one]
apply dvd_zero
·
case succ
i =>
rw [← mul_dvd_mul_iff_left radical_ne_zero, radical_mul_divRadical, radical_pow_of_prime hp i.succ_ne_zero,
derivative_pow_succ, ← mul_assoc]
apply dvd_mul_of_dvd_left
rw [mul_comm, mul_assoc]
apply dvd_mul_of_dvd_right
rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]
· -- If it holds for coprime pair a and b, then it also holds for a * b.
case hcp x y hpxy hx
hy =>
have hc : IsCoprime x y :=
EuclideanDomain.isCoprime_of_dvd
(fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy))) fun p hp _ hpx hpy =>
hp (hpxy hpx hpy)
rw [divRadical_mul hc, derivative_mul]
exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)
