Theorems · Definition · group theory

SubMulAction.conjMap_ofFixingSubgroup

{M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        {s t : Set α} →
          {g : M} →
            (hg : g • t = s) →
              ↥(SubMulAction.ofFixingSubgroup M t) →ₑ[⇑(SubMulAction.fixingSubgroupEquivFixingSubgroup hg)]
                ↥(SubMulAction.ofFixingSubgroup M s)

Conjugation induces an equivariant map between the SubMulAction of the fixing subgroup of a subset and that of a translate.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction