`BookProof.NavierStokesFlow.matrixFlow_commute_of_commute` (t : ℝ) : nsFlowUnitary d t * nsHamiltonian d = nsHamiltonian d * nsFlowUnitary d t
ProvedBookProof.NavierStokesFlow.matrixFlow_commute_of_commutetheoremstimepiece
Prove the following Lean 4 theorem from ChapterNavierStokesCauchy.
BookProof.NavierStokesFlow.matrixFlow_commute_of_commute (t : ℝ) : nsFlowUnitary d t * nsHamiltonian d = nsHamiltonian d * nsFlowUnitary d t
Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.matrixFlow_commute_of_commute.
Preamble
-- Generated from ChapterNavierStokesCauchy.lean — theorem BookProof.NavierStokesFlow.matrixFlow_commute_of_commute
import Mathlib
import Definitions.Def_ChapterNavierStokesCauchy
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow
open scoped BigOperators Matrix Matrix.Norms.Operator
variable {n : ℕ}
variable {n : ℕ} (d : NSTruncation n)Formal statement
theorem BookProof.NavierStokesFlow.matrixFlow_commute_of_commute (t : ℝ) :
nsFlowUnitary d t * nsHamiltonian d = nsHamiltonian d * nsFlowUnitary d t := by sorry