Theorems · Theorem · group theory

Set.conj_mem_fixingSubgroup

∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M},
  g • t = s → ∀ {k : M}, k ∈ fixingSubgroup M t → (MulAut.conj g) k ∈ fixingSubgroup M s

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulAction