English
rootMultiplicity a p equals 0 if p = 0; otherwise it equals the multiplicity of the irreducible factor X − C a in p.
Русский
rootMultiplicity a p равно 0, если p = 0; иначе — кратность фактора X − C a в p.
LaTeX
$$$$ \\operatorname{rootMultiplicity}(a, p) = \\begin{cases} 0, & p = 0, \\\\ \\operatorname{multiplicity}(X - C a, p), & p \\neq 0. \\end{cases} $$$$
Lean4
theorem coeff_divByMonic_X_sub_C_rec (p : R[X]) (a : R) (n : ℕ) :
(p /ₘ (X - C a)).coeff n = coeff p (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1) :=
by
nontriviality R
have := monic_X_sub_C a
set q := p /ₘ (X - C a)
rw [← p.modByMonic_add_div this]
have : degree (p %ₘ (X - C a)) < ↑(n + 1) :=
degree_X_sub_C a ▸ p.degree_modByMonic_lt this |>.trans_le <| WithBot.coe_le_coe.mpr le_add_self
simp [q, sub_mul, add_sub, coeff_eq_zero_of_degree_lt this]
