English
Let p ∈ R[X], q ∈ N, r ∈ A, with p.map(algebraMap R A) = (X − C r)^q · p'. If k < q, then aeval r (derivative^[k] p) = 0.
Русский
Пусть p ∈ R[X], q ∈ N, r ∈ A и p.map(algebraMap R A) = (X − C r)^q · p'. Если k < q, то aeval r (derivative^[k] p) = 0.
LaTeX
$$$$ \text{If } p.map(\text{algebraMap } R A) = (X - C r)^q \cdot p' \text{ and } k < q, \text{ then } \mathrm{aeval}_r(\partial^k p) = 0. $$$$
Lean4
theorem aeval_iterate_derivative_of_lt (p : R[X]) (q : ℕ) (r : A) {p' : A[X]}
(hp : p.map (algebraMap R A) = (X - C r) ^ q * p') {k : ℕ} (hk : k < q) : aeval r (derivative^[k] p) = 0 :=
by
have h (x) : (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1) :=
by
rw [← pow_add, add_tsub_cancel_of_le]
rw [Nat.lt_iff_add_one_le] at hk
exact (le_tsub_of_add_le_left hk).trans (tsub_le_tsub_left (tsub_le_self : _ ≤ k) _)
rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]
simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul, h, ← mul_smul_comm,
mul_assoc, ← mul_sum, eval_mul, pow_one, eval_sub, eval_X, eval_C, sub_self, zero_mul]
