`BookProof.ChapterGaugeIncompleteFixing.isPhysicalOperator_iff_mem_centralizer` (U : G → (H →L[ℂ] H)) (A : H →L[ℂ] H) : IsPhysicalOperator U A ↔ A ∈ Subalgebra.centralizer ℂ (Set.r
ProvedBookProof.ChapterGaugeIncompleteFixing.isPhysicalOperator_iff_mem_centralizertheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeIncompleteFixing.
BookProof.ChapterGaugeIncompleteFixing.isPhysicalOperator_iff_mem_centralizer (U : G → (H →L[ℂ] H)) (A : H →L[ℂ] H) : IsPhysicalOperator U A ↔ A ∈ Subalgebra.centralizer ℂ (Set.range U)
Formalization note: Lean 4 identifier BookProof.ChapterGaugeIncompleteFixing.isPhysicalOperator_iff_mem_centralizer.
Preamble
-- Generated from ChapterGaugeIncompleteFixing.lean — theorem BookProof.ChapterGaugeIncompleteFixing.isPhysicalOperator_iff_mem_centralizer
import Mathlib
import Definitions.Def_ChapterGaugeIncompleteFixing
open BookProof.ChapterGaugeIncompleteFixing
open scoped InnerProductSpace
variable {X : Type*}
variable (G : Type*) [Group G] [MulAction G X]
variable {G : Type*} [Group G]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]Formal statement
theorem BookProof.ChapterGaugeIncompleteFixing.isPhysicalOperator_iff_mem_centralizer (U : G → (H →L[ℂ] H))
(A : H →L[ℂ] H) :
IsPhysicalOperator U A ↔ A ∈ Subalgebra.centralizer ℂ (Set.range U) := by sorry