`BookProof.NavierStokesFlow.FullEsa.diagFullData_hamiltonian` (c : Fin 15 → ℕ → ℝ) (p : Fin 3 → ℕ → ℝ) (nu : ℝ) : (diagFullData c p nu).hamiltonian = diagOp (diagFullSymbol c p nu)

Initializing...

`BookProof.NavierStokesFlow.FullEsa.diagFullData_hamiltonian` (c : Fin 15 → ℕ → ℝ) (p : Fin 3 → ℕ → ℝ) (nu : ℝ) : (diagFullData c p nu).hamiltonian = diagOp (diagFullSymbol c p nu) · Prove2Me