`BookProof.NavierStokesFlow.FullEsa.diagUnboundedData_hamiltonian` : diagUnboundedData.hamiltonian = diagOp (fun n => -(2 * (n : ℝ)))

Initializing...

`BookProof.NavierStokesFlow.FullEsa.diagUnboundedData_hamiltonian` : diagUnboundedData.hamiltonian = diagOp (fun n => -(2 * (n : ℝ))) · Prove2Me