equivFun_symm_single — Mathlib

English

A general form of the previous lemma for Finset sums, showing a decomposition into a single Finsupp element corresponding to i.

Русский

Обобщённая формула для сумм по Finset, которая сводит выражение к одному элементу Finsupp, соответствующему i.

LaTeX

$$$\\text{Finset}.sum\\_single\\_ite(a,i) : \\mathrm{univ}.sum(\\lambda x, \\mathrm{single}_x(\\mathrm{ite}(i=x,a,0))) = \\mathrm{single}_i(a)$$$

Lean4

@[simp]
theorem equivFun_symm_single [Finite n] (b : Basis n R M) (i : n) : b.equivFun.symm (Pi.single i 1) = b i :=
  by
  cases nonempty_fintype n
  simp [Pi.single_apply]

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