The remaining CAR: `{ψ†, ψ†} = 2 ψ†² = 0`
ProvedBookProof.NavierStokes.ghostAnticomm_createghostsnavier-stokestimepiece
The remaining CAR: {ψ†, ψ†} = 2 ψ†² = 0.
Formalization Note. Lean 4 identifier: BookProof.NavierStokes.ghostAnticomm_create (module BookProof.NavierStokes), line-linked source: ChapterNavierStokes.lean lines 102–105.
Preamble
-- Generated from ChapterNavierStokes.lean — theorem BookProof.NavierStokes.ghostAnticomm_create import Mathlib import Definitions.Def_ChapterNavierStokes open BookProof.NavierStokes open Matrix
Formal statement
theorem BookProof.NavierStokes.ghostAnticomm_create :
ghostCreate * ghostCreate + ghostCreate * ghostCreate = 0 := by sorrySource