LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.Module.LinearMap.Defs

theorem LinearMap.map_finsum {ι : Type u_1} {𝕜 : Type u_2} [Semiring 𝕜] {V : Type u_3} [AddCommMonoid V] [Module 𝕜 V] {W : Type u_4} [AddCommMonoid W] [Module 𝕜 W] (f : V →ₗ[𝕜] W) (a : ι → V) (ha : (Function.support a).Finite) : f (∑ᶠ (i : ι), a i) = ∑ᶠ (i : ι), f (a i)