(w : FockL2 K) (hw : ∀ c : Conf K, (inner ℂ ((fockBasis c : FockDom K) : FockL2 K) w : ℂ) = 0) : w = 0

-- Generated from ChapterNavierStokesFockSpace.lean — theorem BookProof.NavierStokesFlow.FockOfFock.innerBasis_total
import Mathlib
import Definitions.Def_ChapterNavierStokesFockSpace
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.FockOfFock








open FullEsa



variable {ι : Type*}














variable {ι : Type*}











variable {M : Type*} [DecidableEq M]

































variable {J K : Type*} [DecidableEq J] [DecidableEq K]

theorem BookProof.NavierStokesFlow.FockOfFock.innerBasis_total (w : FockL2 K)
    (hw : ∀ c : Conf K, (inner ℂ ((fockBasis c : FockDom K) : FockL2 K) w : ℂ) = 0) : w = 0 := by sorry