[DecidableEq ι] (i : ι) : ‖lpBasis (ι

Proved

BookProof.NavierStokesFlow.FockOfFock.norm_lpBasis

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

navier-stokesoperator-algebrastimepiece

Lean 4 theorem BookProof.NavierStokesFlow.FockOfFock.norm_lpBasis (module BookProof.NavierStokesFlow), source chapter BookProof/ChapterNavierStokesFlow.lean.

Preamble

-- Generated from ChapterNavierStokesFockSpace.lean — theorem BookProof.NavierStokesFlow.FockOfFock.norm_lpBasis
import Mathlib
import Definitions.Def_ChapterNavierStokesFockSpace
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.FockOfFock








open FullEsa



variable {ι : Type*}

Formal statement

theorem BookProof.NavierStokesFlow.FockOfFock.norm_lpBasis [DecidableEq ι] (i : ι) : ‖lpBasis (ι := ι) i‖ = 1 := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterNavierStokesFlow.lean

View graph