Commit 2023-01-17 10:45 4b7c58fd

View on Github →

feat: port GroupTheory.Perm.Support (#1614)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/Support.lean

added theorem Equiv.Perm.Disjoint.card_support_mul

added theorem Equiv.Perm.Disjoint.commute

added theorem Equiv.Perm.Disjoint.disjoint_support

added theorem Equiv.Perm.Disjoint.inv_left

added theorem Equiv.Perm.Disjoint.inv_right

added theorem Equiv.Perm.Disjoint.mem_imp

added theorem Equiv.Perm.Disjoint.mono

added theorem Equiv.Perm.Disjoint.mul_apply_eq_iff

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 theorem Equiv.Perm.Disjoint.symmetric

added theorem Equiv.Perm.Disjoint.zpow_disjoint_zpow

added def Equiv.Perm.Disjoint

added theorem Equiv.Perm.IsSwap.of_subtype_isSwap

added def Equiv.Perm.IsSwap

added def Equiv.Perm.Support

added theorem Equiv.Perm.apply_mem_support

added theorem Equiv.Perm.apply_pow_apply_eq_iff

added theorem Equiv.Perm.apply_zpow_apply_eq_iff

added theorem Equiv.Perm.card_support_eq_two

added theorem Equiv.Perm.card_support_eq_zero

added theorem Equiv.Perm.card_support_extend_domain

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.coe_support_eq_set_support

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.eq_on_support_mem_disjoint

added theorem Equiv.Perm.exists_mem_support_of_mem_support_prod

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.ofSubtype_swap_eq

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 theorem Equiv.Perm.pow_eq_on_of_mem_support

added theorem Equiv.Perm.set_support_apply_mem

added theorem Equiv.Perm.set_support_inv_eq

added theorem Equiv.Perm.set_support_mul_subset

added theorem Equiv.Perm.set_support_zpow_subset

added theorem Equiv.Perm.support_congr

added theorem Equiv.Perm.support_eq_empty_iff

added theorem Equiv.Perm.support_extend_domain

added theorem Equiv.Perm.support_inv

added theorem Equiv.Perm.support_le_prod_of_mem

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_subtype_perm

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.support_zpow_le

added theorem Equiv.Perm.two_le_card_support_of_ne_one

added theorem Equiv.Perm.zpow_apply_eq_of_apply_apply_eq_self

added theorem Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self

added theorem Equiv.Perm.zpow_apply_mem_support