LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.BigOperators.FinProd

theorem Finset.sum_eq_sum_support {ι : Type u_1} {R : Type u_2} [AddCommMonoid R] {s : Finset ι} {f : ι → R} (hf : (Function.support f).Finite) (hs : Function.support f ⊆ ↑s) : ∑ i ∈ s, f i = ∑ i ∈ hf.toFinset, f i

theorem Finset.sum_eq_sum_of_support_subset_of_support_subset {ι : Type u_1} {R : Type u_2} [AddCommMonoid R] {s₁ s₂ : Finset ι} {f : ι → R} (hf : (Function.support f).Finite) (hs₁ : Function.support f ⊆ ↑s₁) (hs₂ : Function.support f ⊆ ↑s₂) : ∑ i ∈ s₁, f i = ∑ i ∈ s₂, f i

theorem finsum_add_finsum_compl {V : Type u_1} [AddCommMonoid V] {ι : Type u_2} (I : Set ι) (f : ι → V) (hf : (Function.support f).Finite) : ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι) (_ : i ∈ I), f i + ∑ᶠ (i : ι) (_ : i ∈ Iᶜ), f i