iterate_derivative_X_pow_eq_natCast_mul

English

The derivativeFinsupp of derivative p equals the comapDomain shift of derivativeFinsupp p by Nat.succ, i.e., the index is increased by 1.

Русский

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

LaTeX

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

Lean4

theorem iterate_derivative_X_pow_eq_natCast_mul (n k : ℕ) :
    derivative^[k] (X ^ n : R[X]) = ↑(Nat.descFactorial n k : R[X]) * X ^ (n - k) := by
  induction k with
  | zero => rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
  | succ k
    ih =>
    rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
    simp [mul_assoc, mul_left_comm]

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