Theorems · Theorem · group theory

alternatingGroup.map_kleinFour_conj

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α),
  s.card = 4 →
    ∀ (g : ↥(alternatingGroup α)),
      Subgroup.map (alternatingGroup.ofSubtype (g • s)) (alternatingGroup.kleinFour ↥(g • s)) =
        MulAut.conj g • Subgroup.map (alternatingGroup.ofSubtype s) (alternatingGroup.kleinFour ↥s)

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype