`BookProof.QgCouplingDGammaSum.creVec_finsetSum` (s : Finset ι) (f : ι → (ℕ →₀ ℂ)) (x : FockAlg) : creVec (∑ i ∈ s, f i) x = ∑ i ∈ s, creVec (f i) x

Initializing...

`BookProof.QgCouplingDGammaSum.creVec_finsetSum` (s : Finset ι) (f : ι → (ℕ →₀ ℂ)) (x : FockAlg) : creVec (∑ i ∈ s, f i) x = ∑ i ∈ s, creVec (f i) x · Prove2Me