`BookProof.ChapterG.one_mem_gaugeInvariantSubalgebra` {X Y : Type*} (π : X → Y) : (1 : X → ℝ) ∈ gaugeInvariantSubalgebra ℝ π

Proved

BookProof.ChapterG.one_mem_gaugeInvariantSubalgebra

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterG.

BookProof.ChapterG.one_mem_gaugeInvariantSubalgebra {X Y : Type*} (π : X → Y) : (1 : X → ℝ) ∈ gaugeInvariantSubalgebra ℝ π

Formalization note: Lean 4 identifier BookProof.ChapterG.one_mem_gaugeInvariantSubalgebra.

Preamble

-- Generated from ChapterG.lean — theorem BookProof.ChapterG.one_mem_gaugeInvariantSubalgebra
import Mathlib
import Definitions.Def_ChapterG
open BookProof.ChapterG


open scoped ComplexConjugate InnerProductSpace Matrix

Formal statement

theorem BookProof.ChapterG.one_mem_gaugeInvariantSubalgebra {X Y : Type*} (π : X → Y) :
    (1 : X → ℝ) ∈ gaugeInvariantSubalgebra ℝ π := by sorry

View graph