Commit 2021-04-03 22:50 44f34ee9

View on Github →

feat(group_theory/perm/sign): the alternating group (#6913) Defines alternating_subgroup to be sign.ker Proves a few basic lemmas about its cardinality

Estimated changes

Modified docs/undergrad.yaml

Modified src/group_theory/perm/sign.lean

added def alternating_subgroup

added theorem alternating_subgroup_eq_sign_ker

added theorem alternating_subgroup_normal

added theorem equiv.perm.closure_swaps_eq_top

modified theorem equiv.perm.sign_surjective

added theorem mem_alternating_subgroup

added theorem prod_list_swap_mem_alternating_subgroup_iff_even_length

added theorem two_mul_card_alternating_subgroup

Modified src/group_theory/subgroup.lean