`BookProof.ChapterGaugeIncompleteFixing.no_gauge_invariant_point` [Nontrivial G] (h : MovesEveryPointOfSpectrum G X) (x : X) : ∃ g : G, g • x ≠ x
ProvedBookProof.ChapterGaugeIncompleteFixing.no_gauge_invariant_pointtheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeIncompleteFixing.
BookProof.ChapterGaugeIncompleteFixing.no_gauge_invariant_point [Nontrivial G] (h : MovesEveryPointOfSpectrum G X) (x : X) : ∃ g : G, g • x ≠ x
Formalization note: Lean 4 identifier BookProof.ChapterGaugeIncompleteFixing.no_gauge_invariant_point.
Preamble
-- Generated from ChapterGaugeIncompleteFixing.lean — theorem BookProof.ChapterGaugeIncompleteFixing.no_gauge_invariant_point
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.no_gauge_invariant_point [Nontrivial G] (h : MovesEveryPointOfSpectrum G X)
(x : X) : ∃ g : G, g • x ≠ x := by sorry