`BookProof.ChapterGaugeUnconstrainedSpectrum.signRep_constrainedSpectrum` : constrainedSpectrum signRep = {0}
ProvedBookProof.ChapterGaugeUnconstrainedSpectrum.signRep_constrainedSpectrumtheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeUnconstrainedSpectrum.
BookProof.ChapterGaugeUnconstrainedSpectrum.signRep_constrainedSpectrum : constrainedSpectrum signRep = {0}
Formalization note: Lean 4 identifier BookProof.ChapterGaugeUnconstrainedSpectrum.signRep_constrainedSpectrum.
Preamble
-- Generated from ChapterGaugeUnconstrainedSpectrum.lean — theorem BookProof.ChapterGaugeUnconstrainedSpectrum.signRep_constrainedSpectrum
import Mathlib
import Definitions.Def_ChapterGaugeUnconstrainedSpectrum
import Definitions.Def_ChapterAbelianDiagonalCountable
open BookProof.ChapterAbelianDiagonalCountable
open BookProof.ChapterGaugeUnconstrainedSpectrum
variable {X : Type*}
variable {G : Type*} [Group G]Formal statement
theorem BookProof.ChapterGaugeUnconstrainedSpectrum.signRep_constrainedSpectrum : constrainedSpectrum signRep = {0} := by sorry