Prove2Me

modeShift_shift_ne'

Proved
BookProof.NavierStokesFlow.FockManyMode.modeShift_shift_ne_prime

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

formalizationtimepiece

Formal statement of BookProof.NavierStokesFlow.FockManyMode.modeShift_shift_ne' from the timepiece Lean 4 formalization (source chapter BookProof/ChapterNavierStokesFockManyMode.lean).

Preamble
-- Generated from ChapterNavierStokesFockManyMode.lean — theorem BookProof.NavierStokesFlow.FockManyMode.modeShift_shift_ne'
import Mathlib
import Definitions.Def_ChapterNavierStokesFockManyMode
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.FockManyMode

variable {d : ℕ} {κ : Fin d → ℝ}


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato ShiftHamiltonian
Formal statement
theorem BookProof.NavierStokesFlow.FockManyMode.modeShift_shift_ne_prime (i i₀ : Fin d) :
    modeShift i (modeShift i₀ (0 : Occ d)) ≠ modeShift i₀ 0 := by sorry
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterNavierStokesFockManyMode.lean

View graph