Commit 2021-04-06 09:41 02058ed7

View on Github →

feat(group_theory/perm/*): facts about the cardinality of the support of a permutation (#6951) Proves lemmas about the cardinality of the support of a permutation

Estimated changes

Modified docs/undergrad.yaml

Modified src/group_theory/perm/cycles.lean

added def equiv.perm.cycle_factors

added def equiv.perm.cycle_factors_aux

added theorem equiv.perm.cycle_induction_on

added def equiv.perm.cycle_of

added theorem equiv.perm.is_cycle.ne_one

added theorem equiv.perm.is_cycle.two_le_card_support

deleted theorem equiv.perm.one_lt_nonfixed_point_card_of_ne_one

added def equiv.perm.trunc_cycle_factors

Modified src/group_theory/perm/sign.lean

added theorem equiv.perm.apply_mem_support

added theorem equiv.perm.card_support_eq_two

added theorem equiv.perm.card_support_eq_zero

added theorem equiv.perm.card_support_le_one

added theorem equiv.perm.card_support_ne_one

added theorem equiv.perm.card_support_prod_list_of_pairwise_disjoint

modified theorem equiv.perm.card_support_swap_mul

added theorem equiv.perm.disjoint.card_support_mul

added theorem equiv.perm.disjoint.disjoint_support

added theorem equiv.perm.disjoint.support_mul

added theorem equiv.perm.disjoint_iff_disjoint_support

added theorem equiv.perm.disjoint_prod_list_of_disjoint

added theorem equiv.perm.exists_mem_support_of_mem_support_prod

modified theorem equiv.perm.mem_support

added theorem equiv.perm.one_lt_card_support_of_ne_one

modified def equiv.perm.support

added theorem equiv.perm.support_eq_empty_iff

added theorem equiv.perm.support_inv

added theorem equiv.perm.support_mul_le

added theorem equiv.perm.support_one

modified theorem equiv.perm.support_pow_le

modified theorem equiv.perm.support_swap_mul_eq

added theorem equiv.perm.two_le_card_support_of_ne_one