Alternating Groups #
The alternating group on a finite type α
is the subgroup of the permutation group Perm α
consisting of the even permutations.
Main definitions #
alternatingGroup α
is the alternating group onα
, defined as aSubgroup (Perm α)
.
Main results #
two_mul_card_alternatingGroup
shows that the alternating group is half as large as the permutation group it is a subgroup of.closure_three_cycles_eq_alternating
shows that the alternating group is generated by 3-cycles.alternatingGroup.isSimpleGroup_five
shows that the alternating group onFin 5
is simple. The proof shows that the normal closure of any non-identity element of this group contains a 3-cycle.
Tags #
alternating group permutation
TODO #
- Show that
alternatingGroup α
is simple if and only ifFintype.card α ≠ 4
.
The alternating group on a finite type, realized as a subgroup of Equiv.Perm
.
For alternatingGroup (Fin n)
.
Equations
- alternatingGroup α = Equiv.Perm.sign.ker
Instances For
Equations
Equations
- instUniqueSubtypePermMemSubgroupAlternatingGroupOfSubsingleton α = { default := 1, uniq := ⋯ }
Equations
- ⋯ = ⋯
A key lemma to prove
Part of proving
Equations
- ⋯ = ⋯
The normal closure of the 5-cycle finRotate 5
within
The normal closure of
Shows that any non-identity element of
Shows that