Theorems · Theorem · group theory

AddAction.fixedBy_neg

∀ (α : Type u_1) {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G),
  AddAction.fixedBy α (-g) = AddAction.fixedBy α g

In an additive group action, the points fixed by g are also fixed by g⁻¹

Defined in

Mathlib.GroupTheory.GroupAction.FixedPoints

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddGroupAddAction