`BookProof.ChapterWignerSymmetry.sum_supported` {s : Finset ι} {f : ι → ℂ} (hf : ∀ k, k ∉ s → f k = 0) (g : ι → ℂ) : ∑ k, g k * f k = ∑ k ∈ s, g k * f k

Initializing...

`BookProof.ChapterWignerSymmetry.sum_supported` {s : Finset ι} {f : ι → ℂ} (hf : ∀ k, k ∉ s → f k = 0) (g : ι → ℂ) : ∑ k, g k * f k = ∑ k ∈ s, g k * f k · Prove2Me