Theorems · Definition · group theory

MulAction.stabilizerEquivStabilizer

{G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        {g : G} → {a b : α} → b = g • a → ↥(MulAction.stabilizer G a) ≃* ↥(MulAction.stabilizer G b)

The natural group equivalence between the stabilizers of two elements in the same orbit.

Defined in

Mathlib.GroupTheory.GroupAction.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

GroupMulAction