derivative_pow_succ — Mathlib

English

The derivativeFinsupp of the derivative equals the comapDomain of Nat.succ applied to derivativeFinsupp p, i.e., shifting indices by one.

Русский

ПроизводнаяFinsupp от производной равна сдвигу индексов на 1 через comapDomain Nat.succ.

LaTeX

$$$$ \mathrm{derivativeFinsupp}(\mathrm{derivative}(p)) = \mathrm{comapDomain}(\mathrm{Nat.succ}, \mathrm{injOn}(\mathrm{Nat.succ})) (\mathrm{derivativeFinsupp}(p)) $$$$

Lean4

theorem derivative_pow_succ (p : R[X]) (n : ℕ) : derivative (p ^ (n + 1)) = C (n + 1 : R) * p ^ n * derivative p :=
  Nat.recOn n (by simp) fun n ih => by
    rw [pow_succ, derivative_mul, ih, Nat.add_one, mul_right_comm, C_add, add_mul, add_mul, pow_succ, ← mul_assoc, C_1,
      one_mul];
    simp [add_mul]

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