English
For p ∈ R[X], a ∈ R, and n ∈ ℕ, the coefficient of p /ₘ (X − C a) at n satisfies a recurrence involving coefficients of p at n+1 and a times the coefficient at n+1.
Русский
Для p ∈ R[X], a ∈ R и n ∈ ℕ коэффициент p /ₘ (X − C a) при степени n удовлетворяет рекуррентному соотношению через коэффициенты p при степенях n+1 и a умноженного на коэффициент при n+1.
LaTeX
$$$$ (p /ₘ (X - C a)).\\coeff n = \\operatorname{coeff} p (n + 1) + a \\cdot (p /ₘ (X - C a)).\\coeff (n + 1). $$$$
Lean4
/-- The largest power of `X - C a` which divides `p`.
This *could be* computable via the divisibility algorithm `Polynomial.decidableDvdMonic`,
as shown by `Polynomial.rootMultiplicity_eq_nat_find_of_nonzero` which has a computable RHS. -/
def rootMultiplicity (a : R) (p : R[X]) : ℕ :=
letI := Classical.decEq R
if h0 : p = 0 then 0
else
let _ : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
have := decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1))
inferInstanceAs (Decidable ¬_)
Nat.find (finiteMultiplicity_X_sub_C a h0)
