Commit 2021-04-14 23:14 89196b20

View on Github →

feat(group_theory/perm/cycle_type): Cycle type of a permutation (#6999) This PR defines the cycle type of a permutation. At some point we should prove the bijection between partitions and conjugacy classes.

Estimated changes

Modified src/algebra/gcd_monoid.lean

added theorem nat.gcd_eq_gcd

added theorem nat.lcm_eq_lcm

added theorem nat.normalize_eq

Created src/group_theory/perm/cycle_type.lean

added theorem equiv.perm.card_cycle_type_eq_one

added theorem equiv.perm.card_cycle_type_eq_zero

added def equiv.perm.cycle_type

added theorem equiv.perm.cycle_type_eq

added theorem equiv.perm.cycle_type_eq_zero

added theorem equiv.perm.cycle_type_inv

added theorem equiv.perm.cycle_type_one

added theorem equiv.perm.cycle_type_prime_order

added theorem equiv.perm.disjoint.cycle_type

added theorem equiv.perm.dvd_of_mem_cycle_type

added theorem equiv.perm.is_cycle.cycle_type

added theorem equiv.perm.is_cycle_of_prime_order''

added theorem equiv.perm.is_cycle_of_prime_order'

added theorem equiv.perm.is_cycle_of_prime_order

added theorem equiv.perm.lcm_cycle_type

added theorem equiv.perm.list_cycles_perm_list_cycles

added theorem equiv.perm.mem_list_cycles_iff

added theorem equiv.perm.one_lt_of_mem_cycle_type

added def equiv.perm.partition

added theorem equiv.perm.sign_of_cycle_type

added theorem equiv.perm.sum_cycle_type

added theorem equiv.perm.two_le_of_mem_cycle_type

Modified src/group_theory/perm/cycles.lean

modified theorem equiv.perm.cycle_induction_on

Modified src/group_theory/perm/sign.lean

added theorem equiv.perm.nodup_of_pairwise_disjoint