Prove2Me

canH_crd

Open
BookProof.NavierStokesFlow.CanonicalVector.canH_crd

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

formalizationtimepiece

Formal statement of BookProof.NavierStokesFlow.CanonicalVector.canH_crd from the timepiece Lean 4 formalization (source chapter BookProof/ChapterNavierStokesCanonicalVector.lean).

Preamble
-- Generated from ChapterNavierStokesCanonicalVector.lean — theorem BookProof.NavierStokesFlow.CanonicalVector.canH_crd
import Mathlib
import Definitions.Def_ChapterNavierStokesCanonicalVector
import Definitions.Def_ChapterNavierStokesEsa
import Definitions.Def_ChapterNavierStokesThreeComponent
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.CanonicalVector


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato ThreeComponent ShiftHamiltonian SignedShift

variable (A : Matrix (Fin 3) (Fin 3) ℝ) (c : Fin 3 → ℝ)
Formal statement
theorem BookProof.NavierStokesFlow.CanonicalVector.canH_crd (x : lpFiniteModes Vel) (γ : Vel) :
    crd (canH A c x) γ = canFun A c (crd x) γ := by sorry
Source
https://github.com/leonardpedro/timepiece/blob/61595bc/BookProof/ChapterNavierStokesCanonicalVector.lean

View graph