`BookProof.NavierStokesEulerian.eulerian_divergence_constraint` (u : (Fin 3 → ℝ) → Fin 3 → ℝ) (x : Fin 3 → ℝ) (h : dirDeriv (fun y => u y 2) 2 x = -(dirDeriv (fun y => u y 0) 0 x +

Initializing...

`BookProof.NavierStokesEulerian.eulerian_divergence_constraint` (u : (Fin 3 → ℝ) → Fin 3 → ℝ) (x : Fin 3 → ℝ) (h : dirDeriv (fun y => u y 2) 2 x = -(dirDeriv (fun y => u y 0) 0 x + · Prove2Me