Theorems · Theorem · group theory

MulAction.stabilizerEquivStabilizer_compTriple

∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g h k : G} {a b c : α} {hg : b = g • a}
  {hh : c = h • b} {hk : c = k • a},
  k = h * g →
    CompTriple ⇑(MulAction.stabilizerEquivStabilizer hg) ⇑(MulAction.stabilizerEquivStabilizer hh)
      ⇑(MulAction.stabilizerEquivStabilizer hk)

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulAction