Theorems · Definition · group theory

AddAction.stabilizerEquivStabilizer

{G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        {g : G} → {a b : α} → b = g +ᵥ a → ↥(AddAction.stabilizer G a) ≃+ ↥(AddAction.stabilizer G b)

The isomorphism 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

AddGroupAddAction