The Lean 4 theorem `nsFlow_zero` in the `ChapterNavierStokesFlow` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.nsFlow_zerotimepiece
The Lean 4 theorem nsFlow_zero in the ChapterNavierStokesFlow chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesFlow.lean — theorem BookProof.NavierStokesFlow.nsFlow_zero
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.nsFlow_zero : nsFlowUnitary d 0 = 1 := by sorry
Source