Commit 2021-04-22 20:22 1585b14a

View on Github →

feat(group_theory/perm/*): Generating S_n (#7211) This PR proves several lemmas about generating S_n, culminating in the following result: If H is a subgroup of S_p, and if H has cardinality divisible by p, and if H contains a transposition, then H is all of S_p.

Estimated changes

Modified src/group_theory/perm/cycle_type.lean

added theorem equiv.perm.subgroup_eq_top_of_swap_mem

Modified src/group_theory/perm/cycles.lean

added theorem equiv.perm.closure_cycle_adjacent_swap

added theorem equiv.perm.closure_cycle_coprime_swap

added theorem equiv.perm.closure_is_cycle

added theorem equiv.perm.closure_prime_cycle_swap

deleted theorem equiv.perm.is_cycle.swap

added theorem equiv.perm.is_cycle_swap

added theorem equiv.perm.is_swap.is_cycle

Modified src/group_theory/perm/sign.lean

added theorem equiv.perm.closure_is_swap

deleted theorem equiv.perm.closure_swaps_eq_top

added theorem equiv.perm.support_pow_coprime