: Dense ((FockDom M : Submodule ℂ (FockL2 M)) : Set (FockL2 M))

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








open FullEsa



variable {ι : Type*}














variable {ι : Type*}











variable {M : Type*} [DecidableEq M]

theorem BookProof.NavierStokesFlow.FockOfFock.fockDom_dense : Dense ((FockDom M : Submodule ℂ (FockL2 M)) : Set (FockL2 M)) := by sorry