`BookProof.ChapterGaugeIncompleteFixing.one_mem_physicalSubalgebra` : (1 : X → ℝ) ∈ physicalSubalgebra G
ProvedBookProof.ChapterGaugeIncompleteFixing.one_mem_physicalSubalgebratheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeIncompleteFixing.
BookProof.ChapterGaugeIncompleteFixing.one_mem_physicalSubalgebra : (1 : X → ℝ) ∈ physicalSubalgebra G
Formalization note: Lean 4 identifier BookProof.ChapterGaugeIncompleteFixing.one_mem_physicalSubalgebra.
Preamble
-- Generated from ChapterGaugeIncompleteFixing.lean — theorem BookProof.ChapterGaugeIncompleteFixing.one_mem_physicalSubalgebra
import Mathlib
import Definitions.Def_ChapterGaugeIncompleteFixing
open BookProof.ChapterGaugeIncompleteFixing
open scoped InnerProductSpace
variable {X : Type*}
variable (G : Type*) [Group G] [MulAction G X]Formal statement
theorem BookProof.ChapterGaugeIncompleteFixing.one_mem_physicalSubalgebra : (1 : X → ℝ) ∈ physicalSubalgebra G := by sorry