linearDeriv_apply — Mathlib

English

The explicit application of linear derivatives to coordinates yields the standard expansion form across coordinates.

Русский

Явное применение линейных производных к координатам даёт стандартное разложение через координаты.

LaTeX

$$$ f.linearDeriv_apply (f) (x) (y) = \\sum_i f (update x i (y i)) $$$

Lean4

@[simp]
theorem linearDeriv_apply [DecidableEq ι] [Fintype ι] (f : MultilinearMap R M₁ M₂) (x y : (i : ι) → M₁ i) :
    f.linearDeriv x y = ∑ i, f (update x i (y i)) :=
  by
  unfold linearDeriv
  simp only [LinearMap.coeFn_sum, LinearMap.coe_comp, LinearMap.coe_proj, Finset.sum_apply, Function.comp_apply,
    Function.eval, toLinearMap_apply]

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