The Lean 4 theorem `nsBrst_nilpotent` in the `ChapterNavierStokesFlow` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.nsBrst_nilpotenttimepiece
The Lean 4 theorem nsBrst_nilpotent in the ChapterNavierStokesFlow chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesFlow.lean — theorem BookProof.NavierStokesFlow.nsBrst_nilpotent
import Mathlib
import Definitions.Def_ChapterNavierStokesFlow
open BookProof.NavierStokesFlow
open scoped BigOperators Matrix Kronecker ComplexOrder TensorProduct
variable {n : ℕ} (d : NSTruncation n)Formal statement
theorem BookProof.NavierStokesFlow.nsBrst_nilpotent : nsBrstCharge d * nsBrstCharge d = 0 := by sorry
Source