English
Let p ∈ R[X], q > 0. There exists gp ∈ R[X] such that gp.natDegree ≤ p.natDegree − q and for all r ∈ R, if p = (X − C r)^(q−1) · p' then eval r (sumIDeriv p) = (q−1)! · p'.eval r + q! · eval r gp.
Русский
Пусть p ∈ R[X] и q > 0. Существуют gp ∈ R[X], gp.natDegree ≤ p.natDegree − q такие, что для всех r ∈ R выполняется равенство eval r (sumIDeriv p) = (q−1)! · p'.eval r + q! · eval r gp, если p = (X − C r)^(q−1) · p'.
LaTeX
$$$$ \exists gp ∈ R[X], \; \operatorname{natDegree}(gp) ≤ \operatorname{natDegree}(p) - q \; \wedge\; \forall r ∈ R, \; p = (X - C r)^{q-1} \cdot p' \Rightarrow \mathrm{eval}_r(\mathrm{sumIDeriv} p) = (q - 1)! \cdot p'.\mathrm{eval}_r + q! \cdot \mathrm{eval}_r gp. $$$$
Lean4
theorem eval_sumIDeriv_of_pos [CommRing R] [Nontrivial R] [NoZeroDivisors R] (p : R[X]) {q : ℕ} (hq : 0 < q) :
∃ gp : R[X],
gp.natDegree ≤ p.natDegree - q ∧
∀ (r : R) {p' : R[X]},
p = ((X : R[X]) - C r) ^ (q - 1) * p' → eval r (sumIDeriv p) = (q - 1)! • p'.eval r + q ! • eval r gp :=
by simpa using aeval_sumIDeriv_of_pos R p hq Function.injective_id
