The Lean 4 theorem `nsAdvection_hermitian` in the `ChapterNavierStokesFlow` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.nsAdvection_hermitiantimepiece
The Lean 4 theorem nsAdvection_hermitian in the ChapterNavierStokesFlow chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesFlow.lean — theorem BookProof.NavierStokesFlow.nsAdvection_hermitian
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.nsAdvection_hermitian (i : Fin 3) : (nsAdvection d i)ᴴ = nsAdvection d i := by sorry
Source