Theorems · Theorem · group theory

MulAction.fixedBy_inv

∀ (α : Type u_1) {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G),
  MulAction.fixedBy α g⁻¹ = MulAction.fixedBy α g

In a multiplicative group action, the points fixed by g are also fixed by g⁻¹

Defined in

Mathlib.GroupTheory.GroupAction.FixedPoints

Cited by

4 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

GroupMulAction