`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

Proved

BookProof.NavierStokesEulerian.eulerian_momentum_dual

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesEulerian.

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 then 1 else 0

Formalization note: Lean 4 identifier BookProof.NavierStokesEulerian.eulerian_momentum_dual.

Preamble

-- Generated from ChapterNavierStokesEulerian.lean — theorem BookProof.NavierStokesEulerian.eulerian_momentum_dual
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
import Mathlib
import Definitions.Def_ChapterNavierStokesEulerian
open BookProof.NavierStokesEulerian



open BookProof.NavierStokesFlow Matrix

Formal statement

theorem 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 then 1 else 0 := by sorry

View graph