rootMultiplicity_sub_one_le_derivative_rootMultiplicity

English

For any polynomial p over a CharZero domain R and any t ∈ R, the inequality ord_t(p) − 1 ≤ ord_t(p′) holds.

Русский

Для любого многочлена p над доменом R с характеристикой ноль и любого t ∈ R выполняется неравенство ord_t(p) − 1 ≤ ord_t(p′).

LaTeX

$$$\operatorname{rootMultiplicity}_t(p) - 1 \le \operatorname{rootMultiplicity}_t(p').$$$

Lean4

theorem rootMultiplicity_sub_one_le_derivative_rootMultiplicity [CharZero R] (p : R[X]) (t : R) :
    p.rootMultiplicity t - 1 ≤ p.derivative.rootMultiplicity t :=
  by
  by_cases h : p.IsRoot t
  · exact (derivative_rootMultiplicity_of_root h).symm.le
  · rw [rootMultiplicity_eq_zero h, zero_tsub]
    exact zero_le _

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