Prove2Me

`BookProof.NavierStokesEulerian.u_evaluates_to_value` {E : Type*} [AddCommGroup E] [Module ℂ E] {ι : Type*} [Fintype ι] (u : Fin 3 → E →ₗ[ℂ] E) (uD : Fin 3 → ι → E →ₗ[ℂ] E)...

Proved
BookProof.NavierStokesEulerian.u_evaluates_to_value

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesEulerian.

BookProof.NavierStokesEulerian.u_evaluates_to_value {E : Type*} [AddCommGroup E] [Module ℂ E] {ι : Type*} [Fintype ι] (u : Fin 3 → E →ₗ[ℂ] E) (uD : Fin 3 → ι → E →ₗ[ℂ] E) (X : ι → E →ₗ[ℂ] E) (x : ι → ℂ) (v : E) (hv : ∀ i, X i v = x i • v) (i : Fin 3) : fieldTaylor (u i) (uD i) X x v = u i v

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

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



open BookProof.NavierStokesFlow Matrix
Formal statement
theorem BookProof.NavierStokesEulerian.u_evaluates_to_value {E : Type*} [AddCommGroup E] [Module ℂ E] {ι : Type*} [Fintype ι]
    (u : Fin 3 → E →ₗ[ℂ] E) (uD : Fin 3 → ι → E →ₗ[ℂ] E) (X : ι → E →ₗ[ℂ] E) (x : ι → ℂ)
    (v : E) (hv : ∀ i, X i v = x i • v) (i : Fin 3) :
    fieldTaylor (u i) (uD i) X x v = u i v := by sorry

View graph