The number operator is Hermitian: `Nᴴ = N`

Proved

BookProof.NavierStokes.ghostNumber_hermitian

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

ghostsnavier-stokestimepiece

The number operator is Hermitian: Nᴴ = N.

Formalization Note. Lean 4 identifier: BookProof.NavierStokes.ghostNumber_hermitian (module BookProof.NavierStokes), line-linked source: ChapterNavierStokes.lean lines 116–119.

Preamble

-- Generated from ChapterNavierStokes.lean — theorem BookProof.NavierStokes.ghostNumber_hermitian
import Mathlib
import Definitions.Def_ChapterNavierStokes
open BookProof.NavierStokes












open Matrix

Formal statement

theorem BookProof.NavierStokes.ghostNumber_hermitian : ghostNumberᴴ = ghostNumber := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterNavierStokes.lean#L116-L119

View graph