Commit 2023-04-12 21:22 b99d93c8

View on Github →

feat: port GroupTheory.SpecificGroups.Alternating (#3371)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/SpecificGroups/Alternating.lean

added theorem Equiv.Perm.IsThreeCycle.alternating_normalClosure

added theorem Equiv.Perm.IsThreeCycle.mem_alternatingGroup

added theorem Equiv.Perm.closure_three_cycles_eq_alternating

added theorem Equiv.Perm.finRotate_bit1_mem_alternatingGroup

added theorem Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five

added theorem Equiv.Perm.mem_alternatingGroup

added theorem Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length

added theorem alternatingGroup.isConj_of

added theorem alternatingGroup.isConj_swap_mul_swap_of_cycleType_two

added theorem alternatingGroup.isThreeCycle_isConj

added theorem alternatingGroup.nontrivial_of_three_le_card

added theorem alternatingGroup.normalClosure_finRotate_five

added theorem alternatingGroup.normalClosure_swap_mul_swap_five

added def alternatingGroup

added theorem alternatingGroup_eq_sign_ker

added theorem two_mul_card_alternatingGroup