`BookProof.ChapterG3.free_remnant_moves_every_point` {G Y : Type*} [Group G] [MulAction G Y] (hfree : ∀ (g : G) (y : Y), g • y = y → g = 1) {g : G} (hg : g ≠ 1) (y : Y) : g • y ≠ y

Initializing...

`BookProof.ChapterG3.free_remnant_moves_every_point` {G Y : Type*} [Group G] [MulAction G Y] (hfree : ∀ (g : G) (y : Y), g • y = y → g = 1) {g : G} (hg : g ≠ 1) (y : Y) : g • y ≠ y · Prove2Me