finsuppTotal_apply_eq_of_fintype — Mathlib

English

Let ι be a finite type. For any f in ι →₀ I, the total map sends f to the finite R-linear combination ∑ i (f i) • v i, i.e. finsuppTotal ι M I v f = ∑ i (f i : R) • v i.

Русский

Пусть ι — конечный тип. Для любого f ∈ ι →₀ I отображение finsuppTotal отправляет f в конечную линейную комбинацию элементов v_i с коэффициентами из I: finsuppTotal ι M I v f = ∑ i (f i) • v i.

LaTeX

$$$\\mathrm{finsuppTotal}_{\\iota,M,I,v}\\;f = \\sum_{i} (f(i) : R) \\cdot v(i)$$$

Lean4

theorem finsuppTotal_apply_eq_of_fintype [Fintype ι] (f : ι →₀ I) : finsuppTotal ι M I v f = ∑ i, (f i : R) • v i :=
  by
  rw [finsuppTotal_apply, Finsupp.sum_fintype]
  exact fun _ => zero_smul _ _

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