English
Let h_i be linear maps β2_i → N and f_i: β1_i → β2_i. For l ∈ Π₀ i, β1_i (finite support), the sum after applying mapRange.linearMap equals the sum of the composed maps: ∑_i h_i(f_i(l_i)) = ∑_i (h_i ∘ f_i)(l_i).
Русский
Пусть h_i: β2_i → N и f_i: β1_i → β2_i. Для l с конечной опорой l_i ∈ β1_i выполняется равенство, что сумма по i после применения mapRange.linearMap равна сумме композиция: ∑_i h_i(f_i(l_i)) = ∑_i (h_i ∘ f_i)(l_i).
LaTeX
$$$\\mathrm{lsum}_{\\mathbb{N}}\, h\\, (\\mathrm{mapRange.linearMap}\, f\\, l) = \\mathrm{lsum}_{\\mathbb{N}}\\, (\\lambda i. (h_i) \\circ (f_i))\\, l$$$
Lean4
theorem linearMap [DecidableEq ι] {f : ∀ i, β₁ i →ₗ[R] β₂ i} {h : ∀ i, β₂ i →ₗ[R] N} {l : Π₀ i, β₁ i} :
DFinsupp.lsum ℕ h (mapRange.linearMap f l) = DFinsupp.lsum ℕ (fun i => (h i).comp (f i)) l := by
classical simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp
