LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Finsupp.Supported

theorem finsum_mem_span {ι : Type u_1} {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] (vs : ι → V) (cfs : ι → R) : ∑ᶠ (i : ι), cfs i • vs i ∈ Submodule.span R (Set.range vs)

theorem finsum_mem_mem_span {ι : Type u_1} {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] (vs : ι → V) (cfs : ι → R) (s : Set ι) : ∑ᶠ (i : ι) (_ : i ∈ s), cfs i • vs i ∈ Submodule.span R (vs '' s)