`BookProof.ChapterGaugeComprehensiveFixing.shift_smul_ne_half` {s : ℝ} (hs : s = 0 ∨ s = 1) (g : Multiplicative ℤ) : g • s ≠ (1 / 2 : ℝ)

Initializing...

`BookProof.ChapterGaugeComprehensiveFixing.shift_smul_ne_half` {s : ℝ} (hs : s = 0 ∨ s = 1) (g : Multiplicative ℤ) : g • s ≠ (1 / 2 : ℝ) · Prove2Me