`BookProof.ChapterG.gaugeInvariant_iff_factors` {X Y Z : Type*} {π : X → Y} (hπ : Function.Surjective π) (f : X → Z) : (∀ g ∈ gaugeGroup π, ∀ x, f (g x) = f x) ↔ ∃ h : Y → Z, f = h

Proved

BookProof.ChapterG.gaugeInvariant_iff_factors

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterG.

BookProof.ChapterG.gaugeInvariant_iff_factors {X Y Z : Type*} {π : X → Y} (hπ : Function.Surjective π) (f : X → Z) : (∀ g ∈ gaugeGroup π, ∀ x, f (g x) = f x) ↔ ∃ h : Y → Z, f = h ∘ π

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

Preamble

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


open scoped ComplexConjugate InnerProductSpace Matrix

Formal statement

theorem BookProof.ChapterG.gaugeInvariant_iff_factors {X Y Z : Type*} {π : X → Y}
    (hπ : Function.Surjective π) (f : X → Z) :
    (∀ g ∈ gaugeGroup π, ∀ x, f (g x) = f x) ↔ ∃ h : Y → Z, f = h ∘ π := by sorry

View graph