Prove2Me

(j : J) (c : Conf K) : creat (j, c) (vacuum : FockOfFockDom J K) = fockBasis (Finsupp.single (j, c) 1)

Proved
BookProof.NavierStokesFlow.FockOfFock.outerOneParticle

by leonardopedro · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

navier-stokesoperator-algebrastimepiece

Lean 4 theorem BookProof.NavierStokesFlow.FockOfFock.outerOneParticle (module BookProof.NavierStokesFlow), source chapter BookProof/ChapterNavierStokesFlow.lean.

Preamble
-- Generated from ChapterNavierStokesFockSpace.lean — theorem BookProof.NavierStokesFlow.FockOfFock.outerOneParticle
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]
Formal statement
theorem BookProof.NavierStokesFlow.FockOfFock.outerOneParticle (j : J) (c : Conf K) :
    creat (j, c) (vacuum : FockOfFockDom J K) = fockBasis (Finsupp.single (j, c) 1) := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterNavierStokesFlow.lean

View graph