The number operator is a projection: `N² = N`; its eigenvalues are `0` and `1`, the fermionic occupation numbers
ProvedBookProof.NavierStokes.ghostNumber_idemghostsnavier-stokestimepiece
The number operator is a projection: N² = N; its eigenvalues are 0 and
1, the fermionic occupation numbers.
Formalization Note. Lean 4 identifier: BookProof.NavierStokes.ghostNumber_idem (module BookProof.NavierStokes), line-linked source: ChapterNavierStokes.lean lines 121–126.
Preamble
-- Generated from ChapterNavierStokes.lean — theorem BookProof.NavierStokes.ghostNumber_idem import Mathlib import Definitions.Def_ChapterNavierStokes open BookProof.NavierStokes open Matrix
Formal statement
theorem BookProof.NavierStokes.ghostNumber_idem : ghostNumber * ghostNumber = ghostNumber := by sorry
Source