hasseDeriv_apply — Mathlib

English

The hasseDeriv has a concrete coefficient expression: coeff of the hasseDeriv is (n choose k) times coefficient of f at n+k.

Русский

Коэффициенты hasseDeriv выражаются через биномиальные коэффициенты: (n k) f_{n+k}.

LaTeX

$$$(hasseDeriv\ k\ f).coeff\ n = \binom{n+k}{k}\cdot f_{n+k}$.$$

Lean4

theorem hasseDeriv_apply : hasseDeriv k f = f.sum fun i r => monomial (i - k) (↑(i.choose k) * r) :=
  by
  dsimp [hasseDeriv]
  simp

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