lsum_single — Mathlib

English

There is a linear equivalence induced by a domain equivalence of functions with finite support.

Русский

Существует линейное эквивалентное отображение, индуцируемое эквиваленцией домена для функций с конечной поддержкой.

LaTeX

$$$$ \text{Finsupp}.\text{domLCongr}(e) : (\alpha \to_0 M) \cong_\mathrm{linear} (\alpha' \to_0 M) $$$$

Lean4

theorem lsum_single (f : α → M →ₛₗ[σ] N) (i : α) (m : M) : Finsupp.lsum S f (Finsupp.single i m) = f i m :=
  Finsupp.sum_single_index (f i).map_zero

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