`BookProof.QgCouplingDGammaSum.commForm_finsetSum` {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] {D : Submodule ℂ F} (s : Finset ι) (H : ι → D →ₗ[ℂ] F) (N : D →ₗ[ℂ] F)
ProvedBookProof.QgCouplingDGammaSum.commForm_finsetSumtheoremstimepiece
Prove the following Lean 4 theorem from ChapterQgCouplingDGammaSum.
BookProof.QgCouplingDGammaSum.commForm_finsetSum {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] {D : Submodule ℂ F} (s : Finset ι) (H : ι → D →ₗ[ℂ] F) (N : D →ₗ[ℂ] F) (x : D) : commForm (∑ i ∈ s, H i) N x = ∑ i ∈ s, commForm (H i) N x
Formalization note: Lean 4 identifier BookProof.QgCouplingDGammaSum.commForm_finsetSum.
Preamble
-- Generated from ChapterQgCouplingDGammaSum.lean — theorem BookProof.QgCouplingDGammaSum.commForm_finsetSum
import Definitions.Def_ChapterFockSecondQuantization
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
import Definitions.Def_ChapterNavierStokesIkebeKato
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterFriedrichsExtension
import Definitions.Def_ChapterYangMillsFriedrichs
import Mathlib
import Definitions.Def_ChapterQgCouplingDGammaSum
import Definitions.Def_ChapterFarisLavineCore
open BookProof.QgCouplingDGammaSum
open BookProof.FockSecondQuantization
open BookProof.NavierStokesFlow BookProof.NavierStokesFlow.IkebeKato
open BookProof.FarisLavine BookProof.FriedrichsExtension BookProof.YangMillsFriedrichs
noncomputable section
variable {ι : Type*}Formal statement
theorem BookProof.QgCouplingDGammaSum.commForm_finsetSum {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
{D : Submodule ℂ F} (s : Finset ι) (H : ι → D →ₗ[ℂ] F) (N : D →ₗ[ℂ] F) (x : D) :
commForm (∑ i ∈ s, H i) N x = ∑ i ∈ s, commForm (H i) N x := by sorry