Theorems · Theorem · group theory

MulAction.stabilizerEquivStabilizer_apply

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a)
  (x : ↥(MulAction.stabilizer G a)), ↑((MulAction.stabilizerEquivStabilizer hg) x) = (MulAut.conj g) ↑x

Defined in

Mathlib.GroupTheory.GroupAction.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction