`BookProof.ChapterG2.no_continuous_gauge_fixing_circle` : ¬ ∃ s : Circle → ℝ, Continuous s ∧ ∀ z, Circle.exp (s z) = z

Initializing...

`BookProof.ChapterG2.no_continuous_gauge_fixing_circle` : ¬ ∃ s : Circle → ℝ, Continuous s ∧ ∀ z, Circle.exp (s z) = z · Prove2Me