`BookProof.NavierStokesEulerian.eulerian_momentum_dual` (i j k l : Fin 3) : (MvPolynomial.pderiv (i, j)) (MvPolynomial.X (k, l) : MvPolynomial (Fin 3 × Fin 3) ℂ) = if i = k ∧ j = l

Initializing...

`BookProof.NavierStokesEulerian.eulerian_momentum_dual` (i j k l : Fin 3) : (MvPolynomial.pderiv (i, j)) (MvPolynomial.X (k, l) : MvPolynomial (Fin 3 × Fin 3) ℂ) = if i = k ∧ j = l · Prove2Me