Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-07 15:40 e55d470c

View on Github →

feat(specific_groups/alternating_group): The alternating group on 5 elements is simple (#7502) Shows that is_simple_group (alternating_group (fin 5))

Estimated changes

Modified src/data/multiset/basic.lean

added theorem multiset.le_sum_of_mem

Modified src/group_theory/perm/cycle_type.lean

added theorem equiv.perm.cycle_type_of_card_le_mem_cycle_type_add_two

added theorem equiv.perm.is_three_cycle.is_three_cycle_sq

added theorem equiv.perm.is_three_cycle.order_of

added theorem equiv.perm.le_card_support_of_mem_cycle_type

added theorem equiv.perm.mem_cycle_type_iff

Modified src/group_theory/specific_groups/alternating.lean

added theorem alternating_group.is_conj_swap_mul_swap_of_cycle_type_two

added theorem alternating_group.nontrivial_of_three_le_card

added theorem alternating_group.normal_closure_swap_mul_swap_five

added theorem equiv.perm.is_three_cycle_sq_of_three_mem_cycle_type_five

Modified src/group_theory/subgroup.lean

added theorem is_conj.normal_closure_eq_top_of

added theorem monoid_hom.cod_restrict_apply