Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 95b91b38

View on Github →

refactor(group_theory/perm/*): disjoint and support in own file (#7450) The group_theory/perm/sign file was getting large and too broad in scope. This refactor pulls out perm.support, perm.is_swap, and perm.disjoint into a separate file. A simpler version of #7118.

Estimated changes

Modified src/group_theory/perm/cycle_type.lean

Modified src/group_theory/perm/cycles.lean

Modified src/group_theory/perm/sign.lean

deleted theorem equiv.perm.apply_mem_support

deleted theorem equiv.perm.card_support_eq_two

deleted theorem equiv.perm.card_support_eq_zero

deleted theorem equiv.perm.card_support_le_one

deleted theorem equiv.perm.card_support_ne_one

deleted theorem equiv.perm.card_support_prod_list_of_pairwise_disjoint

deleted theorem equiv.perm.card_support_swap

deleted theorem equiv.perm.card_support_swap_mul

deleted theorem equiv.perm.disjoint.card_support_mul

deleted theorem equiv.perm.disjoint.disjoint_support

deleted theorem equiv.perm.disjoint.gpow_disjoint_gpow

deleted theorem equiv.perm.disjoint.mul_apply_eq_iff

deleted theorem equiv.perm.disjoint.mul_comm

deleted theorem equiv.perm.disjoint.mul_eq_one_iff

deleted theorem equiv.perm.disjoint.mul_left

deleted theorem equiv.perm.disjoint.mul_right

deleted theorem equiv.perm.disjoint.pow_disjoint_pow

deleted theorem equiv.perm.disjoint.support_mul

deleted theorem equiv.perm.disjoint.symm

deleted def equiv.perm.disjoint

deleted theorem equiv.perm.disjoint_comm

deleted theorem equiv.perm.disjoint_iff_disjoint_support

deleted theorem equiv.perm.disjoint_one_left

deleted theorem equiv.perm.disjoint_one_right

deleted theorem equiv.perm.disjoint_prod_list_of_disjoint

deleted theorem equiv.perm.disjoint_prod_perm

deleted theorem equiv.perm.disjoint_prod_right

deleted theorem equiv.perm.exists_mem_support_of_mem_support_prod

deleted theorem equiv.perm.gpow_apply_eq_of_apply_apply_eq_self

deleted theorem equiv.perm.gpow_apply_eq_self_of_apply_eq_self

deleted theorem equiv.perm.gpow_apply_mem_support

deleted theorem equiv.perm.is_swap.of_subtype_is_swap

deleted def equiv.perm.is_swap

deleted theorem equiv.perm.mem_support

deleted theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self

deleted theorem equiv.perm.nodup_of_pairwise_disjoint

deleted theorem equiv.perm.one_lt_card_support_of_ne_one

deleted theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self

deleted theorem equiv.perm.pow_apply_eq_self_of_apply_eq_self

deleted theorem equiv.perm.pow_apply_mem_support

deleted def equiv.perm.support

deleted theorem equiv.perm.support_eq_empty_iff

deleted theorem equiv.perm.support_inv

deleted theorem equiv.perm.support_mul_le

deleted theorem equiv.perm.support_one

deleted theorem equiv.perm.support_pow_le

deleted theorem equiv.perm.support_swap

deleted theorem equiv.perm.support_swap_mul_eq

deleted theorem equiv.perm.two_le_card_support_of_ne_one

Created src/group_theory/perm/support.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

added theorem equiv.perm.card_support_swap

added 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.gpow_disjoint_gpow

added theorem equiv.perm.disjoint.inv_left

added theorem equiv.perm.disjoint.inv_right

added theorem equiv.perm.disjoint.mul_apply_eq_iff

added theorem equiv.perm.disjoint.mul_comm

added theorem equiv.perm.disjoint.mul_eq_one_iff

added theorem equiv.perm.disjoint.mul_left

added theorem equiv.perm.disjoint.mul_right

added theorem equiv.perm.disjoint.pow_disjoint_pow

added theorem equiv.perm.disjoint.support_mul

added theorem equiv.perm.disjoint.symm

added def equiv.perm.disjoint

added theorem equiv.perm.disjoint_comm

added theorem equiv.perm.disjoint_iff_disjoint_support

added theorem equiv.perm.disjoint_iff_eq_or_eq

added theorem equiv.perm.disjoint_inv_left_iff

added theorem equiv.perm.disjoint_inv_right_iff

added theorem equiv.perm.disjoint_one_left

added theorem equiv.perm.disjoint_one_right

added theorem equiv.perm.disjoint_prod_perm

added theorem equiv.perm.disjoint_prod_right

added theorem equiv.perm.disjoint_refl_iff

added theorem equiv.perm.exists_mem_support_of_mem_support_prod

added theorem equiv.perm.gpow_apply_eq_of_apply_apply_eq_self

added theorem equiv.perm.gpow_apply_eq_self_of_apply_eq_self

added theorem equiv.perm.gpow_apply_mem_support

added theorem equiv.perm.is_swap.of_subtype_is_swap

added def equiv.perm.is_swap

added theorem equiv.perm.mem_support

added theorem equiv.perm.mem_support_swap_mul_imp_mem_support_ne

added theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self

added theorem equiv.perm.nodup_of_pairwise_disjoint

added theorem equiv.perm.not_mem_support

added theorem equiv.perm.one_lt_card_support_of_ne_one

added theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self

added theorem equiv.perm.pow_apply_eq_self_of_apply_eq_self

added theorem equiv.perm.pow_apply_mem_support

added def equiv.perm.support

added theorem equiv.perm.support_congr

added theorem equiv.perm.support_eq_empty_iff

added theorem equiv.perm.support_gpow_le

added theorem equiv.perm.support_inv

added theorem equiv.perm.support_mul_le

added theorem equiv.perm.support_one

added theorem equiv.perm.support_pow_le

added theorem equiv.perm.support_prod_le

added theorem equiv.perm.support_prod_of_pairwise_disjoint

added theorem equiv.perm.support_refl

added theorem equiv.perm.support_swap

added theorem equiv.perm.support_swap_iff

added theorem equiv.perm.support_swap_mul_eq

added theorem equiv.perm.support_swap_mul_ge_support_diff

added theorem equiv.perm.support_swap_mul_swap

added theorem equiv.perm.two_le_card_support_of_ne_one