The Lean 4 theorem `fieldPoly_polySym` in the `ChapterNavierStokesDiffHashimoto` chapter of the timepiece formalization

Proved

BookProof.NavierStokesFlow.DiffHashimoto.fieldPoly_polySym

by leonardopedro · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem fieldPoly_polySym in the ChapterNavierStokesDiffHashimoto chapter of the timepiece formalization.

Preamble

-- Generated from ChapterNavierStokesDiffHashimoto.lean — theorem BookProof.NavierStokesFlow.DiffHashimoto.fieldPoly_polySym
import Mathlib
import Definitions.Def_ChapterNavierStokesDiffHashimoto
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.DiffHashimoto







open Filter Topology



open MvPolynomial
open BookProof.FarisLavine BookProof.HashimotoShiftInvert BookProof.EsaClosure
open BookProof.HermiteGalerkin
open BookProof.HermiteProductCore BookProof.HermiteProductBasis
open BookProof.HermiteRelative
open BookProof.NavierStokesFlow.DifferentialL2

noncomputable section

variable (A : Matrix (Fin 3) (Fin 3) ℝ) (c : Fin 3 → ℝ)

Formal statement

theorem BookProof.NavierStokesFlow.DiffHashimoto.fieldPoly_polySym (i : Fin 3) :
    BookProof.YangMillsHermite.PolySym (fieldPoly A c i) := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterNavierStokesDiffHashimoto.lean

View graph