hasseDeriv_single_add — Mathlib

English

The derivative of a single basis element is another single basis element with a shifted index and scaled coefficient.

Русский

Производная по Хассе базисного элемента есть элемент с другим индексом и масштабированным коэффициентом.

LaTeX

$$hasseDeriv R k (single (n+k) x) = single n (binom{n+k}{k} • x)$$

Lean4

theorem hasseDeriv_single_add (k : ℕ) (n : ℤ) (x : V) :
    hasseDeriv R k (single (n + k) x) = single n ((Ring.choose (n + k) k) • x) :=
  by
  ext m
  dsimp only [hasseDeriv_coeff]
  by_cases h : m = n
  · simp [h]
  · simp [h, show m + k ≠ n + k by cutsat]

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