English
Let R be a domain of characteristic zero and p ∈ R[X]. If t ∈ R is a root of p and p ≠ 0, then the root multiplicity of t for p′ is exactly one less than that for p: ord_t(p′) = ord_t(p) − 1.
Русский
Пусть R — область без нуля характеристика ноль, p ∈ R[X]. Если t ∈ R является корнем p и p ≠ 0, то кратность корня t у p′ ровно на единицу меньше кратности корня t у p: ord_t(p′) = ord_t(p) − 1.
LaTeX
$$$ p \neq 0 \ \wedge\ \ p(t)=0 \implies \operatorname{rootMultiplicity}_t(p')= \operatorname{rootMultiplicity}_t(p)-1. $$$
Lean4
theorem derivative_rootMultiplicity_of_root [CharZero R] {p : R[X]} {t : R} (hpt : p.IsRoot t) :
p.derivative.rootMultiplicity t = p.rootMultiplicity t - 1 :=
by
by_cases h : p = 0
· rw [h, map_zero, rootMultiplicity_zero]
exact
derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors hpt <|
mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 ((rootMultiplicity_pos h).2 hpt).ne'
