pow_rootMultiplicity_dvd — Mathlib

English

For p and a, the division by X − C a yields a recurrence for coefficients: coeff of p /ₘ (X − C a) at n equals sum over i from n+1 to natDegree p of a^(i−(n+1)) times p.coeff i.

Русский

Для p и a деление на X − C a задаёт рекуррентность коэффициентов: coeff(p /ₘ (X − C a))_n = ∑_{i = n+1}^{natDegree p} a^{i−(n+1)} p.coeff i.

LaTeX

$$$$ (p /ₘ (X - C a)).coeff n = \\sum_{i = \\mathrm{Icc}(n+1, p.natDegree)} a^{i - (n+1)} \\cdot p.coeff i. $$$$

Lean4

theorem pow_rootMultiplicity_dvd (p : R[X]) (a : R) : (X - C a) ^ rootMultiplicity a p ∣ p :=
  letI := Classical.decEq R
  if h : p = 0 then by simp [h]
  else by classical rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvd

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