Theorems · Theorem · group theory
alternatingGroup.isConj_swap_mul_swap_of_cycleType_two
Deprecated since 2026-04-28Mathlib marks this declaration as deprecated.
∀ {g : Equiv.Perm (Fin 5)},
g ∈ alternatingGroup (Fin 5) → g ≠ 1 → (∀ n ∈ g.cycleType, n = 2) → IsConj (Equiv.swap 0 4 * Equiv.swap 1 3) gShows that any non-identity element of $A_5$ whose cycle decomposition consists only of swaps is conjugate to $(04)(13)$. This is used to show that the normal closure of such a permutation in $A_5$ is $A_5$.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites43
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- Subgroupstatement · cited by 3,593
- one_mulproof · cited by 2,841
- Unitsproof · cited by 2,804
- Multisetstatement and proof · cited by 2,627
- Finset.cardproof · cited by 2,327
- Disjointproof · cited by 2,201
- le_antisymmproof · cited by 2,068
- Fintype.cardproof · cited by 1,386
- Equiv.Permstatement and proof · cited by 1,375
- le_transproof · cited by 985
- Evenproof · cited by 444
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.