English
Let I be an ideal of R, M an R-module, v a family of elements of M indexed by ι, and f ∈ ι →₀ I be a finitely supported function into I. Then finsuppTotal ι M I v f equals the finite R-linear combination of the v_i with coefficients f(i) viewed as elements of R; i.e., finsuppTotal ι M I v f = ∑ i x => (f i) • v_i with x := f i.
Русский
Пусть I — идеал кольца R, M — модуль над R, v — семейство элементов M индексировано i ∈ ι, и f ∈ ι →₀ I. Тогда finsuppTotal ι M I v f равен конечному линейному сочетанию компонент v_i с коэффициентами f(i) (взятыми как элементы R): finsuppTotal ι M I v f = ∑ i (f i : R) • v_i.
LaTeX
$$$ \text{finsuppTotal}_{\iota} (M) (I) (v) (f) = \sum_{i} (f(i) : R) \; v_i. $$$
Lean4
theorem finsuppTotal_apply (f : ι →₀ I) : finsuppTotal ι M I v f = f.sum fun i x => (x : R) • v i :=
by
dsimp [finsuppTotal]
rw [Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]
exact fun _ => zero_smul _ _
