Theorems · Theorem · group theory

SubMulAction.ofStabilizer.conjMap_comp

∀ {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) (H : k = h * g),
  (SubMulAction.ofStabilizer.conjMap hh).comp (SubMulAction.ofStabilizer.conjMap hg) =
    SubMulAction.ofStabilizer.conjMap hk

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Cited by

0 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMulAction