rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero

English

If p has a root at t and p.rootMultiplicity t is not a zero divisor, then the derivative reduces root multiplicity by one: (derivative p).rootMultiplicity t = p.rootMultiplicity t - 1.

Русский

Если p имеет корень в t и p.rootMultiplicity t не является нулевым делителем, кратность корня у производной уменьшается на 1.

LaTeX

$$$$ (\mathrm{derivative}\, p).\mathrm{rootMultiplicity}\, t = p.\mathrm{rootMultiplicity}\, t - 1 $$$$

Lean4

theorem rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero (p : R[X]) (t : R)
    (hnezero : derivative p ≠ 0) : p.rootMultiplicity t - 1 ≤ p.derivative.rootMultiplicity t :=
  (le_rootMultiplicity_iff hnezero).2 <| pow_sub_one_dvd_derivative_of_pow_dvd (p.pow_rootMultiplicity_dvd t)

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