`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

Initializing...

`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 · Prove2Me