Commit 2021-05-07 22:54 515fb2f0

feat(group_theory/perm/*): lemmas about extend_domain, fin_rotate, and fin.cycle_type (#7447) Shows how disjoint, support, is_cycle, and cycle_type behave under extend_domain Calculates support and cycle_type for fin_rotate and fin.cycle_type Shows that the normal closure of fin_rotate 5 in alternating_group (fin 5) is the whole alternating group.