mathlib3

515fb2f0 - feat(group_theory/perm/*): lemmas about `extend_domain`, `fin_rotate`, and `fin.cycle_type` (#7447)

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. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>