Support

📁 Source: Mathlib/GroupTheory/Perm/Support.lean

Statistics

Metric	Count
Definitions IsSwap, support	2
Theorems card_support_mul, commute, conj, disjoint_support, inv_left, inv_right, mem_imp, mono, mul_apply_eq_iff, mul_eq_one_iff, mul_left, mul_right, pow_disjoint_pow, support_mul, symmetric, zpow_disjoint_zpow, of_subtype_isSwap, apply_mem_support, apply_pow_apply_eq_iff, apply_zpow_apply_eq_iff, card_support_conj, card_support_eq_two, card_support_eq_zero, card_support_extend_domain, card_support_le_one, card_support_ne_one, card_support_prod_list_of_pairwise_disjoint, card_support_swap, card_support_swap_mul, coe_support_eq_set_support, disjoint_comm, disjoint_conj, disjoint_iff_disjoint_support, disjoint_iff_eq_or_eq, disjoint_inv_left_iff, disjoint_inv_right_iff, disjoint_noncommProd_right, disjoint_one_left, disjoint_one_right, disjoint_prod_perm, disjoint_prod_right, disjoint_refl_iff, disjoint_swap_swap, eq_on_support_mem_disjoint, exists_mem_support_of_mem_support_prod, fixed_point_card_lt_of_ne_one, instSymmDisjoint, isInvariant_of_support_le, mem_support, mem_support_iff_of_commute, mem_support_of_mem_noncommProd_support, mem_support_swap_mul_imp_mem_support_ne, ne_and_ne_of_swap_mul_apply_ne_self, nodup_of_pairwise_disjoint, notMem_support, ofSubtype_eq_iff, ofSubtype_swap_eq, one_lt_card_support_of_ne_one, pow_apply_eq_of_apply_apply_eq_self, pow_apply_eq_self_of_apply_eq_self, pow_apply_mem_support, pow_eq_on_of_mem_support, set_support_apply_mem, set_support_inv_eq, set_support_mul_subset, set_support_symm_eq, set_support_zpow_subset, support_congr, support_conj, support_eq_empty_iff, support_extend_domain, support_inv, support_le_prod_of_mem, support_mul_le, support_noncommProd, support_ofSubtype, support_one, support_pow_le, support_prod_le, support_prod_of_pairwise_disjoint, support_refl, support_subtypePerm, support_swap, support_swap_iff, support_swap_mul_eq, support_swap_mul_ge_support_diff, support_swap_mul_swap, support_zpow_le, two_le_card_support_of_ne_one, zpow_apply_eq_of_apply_apply_eq_self, zpow_apply_eq_self_of_apply_eq_self, zpow_apply_mem_support	92
Total	94

Equiv.Perm

Definitions

Name	Category	Theorems
IsSwap 📖	MathDef	8 math math: closure_isSwap, mem_closure_isSwap', swap_isSwap_iff, isSwap_iff_cycleType, Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia, card_support_eq_two, mclosure_isSwap, has_swap_mem_of_lt_stabilizer
support 📖	CompOp	119 math math: support_closure_subset_union, SameCycle.exists_pow_eq, mem_toList_iff, List.support_formPerm_le, support_prod_of_pairwise_disjoint, cycleType_eq', card_support_swap_mul, card_support_le_one, cycleType_eq, support_eq_empty_iff, IsCycle.nonempty_support, notMem_support, OnCycleFactors.mem_range_toPermHom_iff', support_cycleOf_le, Basis.mem_support_self', mem_support_iff_of_commute, support_one, support_cycleOf_nonempty, IsThreeCycle.support_eq_iff_mem_support, SameCycle.mem_support_iff, card_support_eq_zero, IsCycle.commute_iff', support_pow_le, isCycleOn_support_cycleOf, support_swap_mul_eq, zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff, support_swap_mul_swap, Disjoint.card_support_mul, commute_iff_of_mem_cycleFactorsFinset, coe_support_eq_set_support, mem_support_cycle_of_cycle, mem_support, two_le_card_support_of_ne_one, mem_support_cycleOf_iff, Basis.card_ofPermHom_support, mem_support_iff_mem_support_of_mem_cycleFactorsFinset, mem_support_cycleOf_iff', Cycle.support_formPerm, Disjoint.support_mul, IsThreeCycle.card_support, support_swap_iff, OnCycleFactors.mem_range_toPermHom'_iff, support_noncommProd, support_cycleOf_eq_nil_iff, toList_eq_nil_iff, IsCycle.cycleType, mem_cycleType_iff, support_zpowers_of_mem_cycleFactorsFinset_le, one_lt_card_support_of_ne_one, support_ofSubtype, IsCycle.support_pow_eq_iff, support_zpow_le, Basis.mem_support_self, support_extend_domain, IsCycle.orderOf, support_mul_le, card_support_prod_list_of_pairwise_disjoint, List.support_formPerm_of_nodup, card_compl_support_modEq, zpow_apply_mem_support, card_support_extend_domain, le_card_support_of_mem_cycleType, Basis.ofPermHom_support, IsThreeCycle.eq_swap_mul_swap_iff_mem_support, support_swap_mul_ge_support_diff, Basis.ofPermHomFun_apply_mem_support_cycle_iff, card_support_swap, support_inv, zpow_eq_zpow_on_iff, IsCycle.zpowersEquivSupport_apply, support_finRotate, IsCycle.support_pow_of_pos_of_lt_orderOf, mem_cycleFactorsFinset_support, pow_apply_mem_support, isPretransitive_of_isCycle_mem, IsThreeCycle.nodup_iff_mem_support, card_support_eq_three_iff, Disjoint.disjoint_support, support_prod_le, support_conj, pow_mod_card_support_cycleOf_self_apply, pow_apply_mem_toList_iff_mem_support, subtypePerm_on_cycleFactorsFinset, apply_mem_support, OnCycleFactors.mem_range_toPermHom_iff, support_pow_coprime, ofSubtype_eq_iff, support_finRotate_of_le, support_refl, cycleOf_mem_cycleFactorsFinset_iff, IsCycle.zpowersEquivSupport_symm_apply, card_support_conj, IsCycle.two_le_card_support, two_le_card_support_cycleOf_iff, two_dvd_card_support, support_swap, IsCycle.sign, card_support_eq_two, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, IsCycle.forall_commute_iff, parts_partition, cycleType_def, length_toList, eq_cycleOf_of_mem_cycleFactorsFinset_iff, two_le_length_toList_iff_mem_support, IsCycle.commute_iff, CycleType.count_def, ofSubtype_support_disjoint, isCycleOn_support_of_mem_cycleFactorsFinset, sum_cycleType, cycle_zpow_mem_support_iff, List.zipWith_swap_prod_support, mem_cycleFactorsFinset_support_le, mem_conj_support, disjoint_iff_disjoint_support, support_le_prod_of_mem, support_subtypePerm, Finset.exists_cycleOn, IsCycle.isConj_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mem_support 📖	mathematical	—	Finset Finset.instMembership support DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	mem_support Equiv.apply_eq_iff_eq
apply_pow_apply_eq_iff 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instPowNat	—	mul_apply Commute.self_pow Equiv.apply_eq_iff_eq
apply_zpow_apply_eq_iff 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike DivInvMonoid.toZPow Group.toDivInvMonoid permGroup	—	mul_apply Commute.self_zpow Equiv.apply_eq_iff_eq
card_support_conj 📖	mathematical	—	Finset.card support Equiv.Perm instMul instInv	—	support_conj Finset.card_map
card_support_eq_two 📖	mathematical	—	Finset.card support IsSwap	—	Finset.card_eq_succ Finset.card_eq_one Finset.mem_singleton ext mem_support Finset.mem_insert Equiv.swap_apply_of_ne_of_ne Equiv.apply_eq_iff_eq Equiv.swap_apply_left Equiv.swap_apply_right card_support_swap
card_support_eq_zero 📖	mathematical	—	Finset.card support Equiv.Perm instOne	—	Finset.card_eq_zero support_eq_empty_iff
card_support_extend_domain 📖	mathematical	—	Finset.card support extendDomain	—	support_extend_domain Finset.card_map
card_support_le_one 📖	mathematical	—	Finset.card support Equiv.Perm instOne	—	le_iff_lt_or_eq card_support_eq_zero card_support_ne_one
card_support_ne_one 📖	—	—	—	—	ne_of_eq_of_ne card_support_eq_zero zero_ne_one ne_of_gt one_lt_card_support_of_ne_one
card_support_prod_list_of_pairwise_disjoint 📖	mathematical	Equiv.Perm Disjoint	Finset.card support instMul instOne AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid Finset	—	card_support_eq_zero Disjoint.card_support_mul disjoint_prod_right
card_support_swap 📖	mathematical	—	Finset.card support Equiv.swap	—	Multiset.nodup_cons support_swap Finset.cons_eq_insert
card_support_swap_mul 📖	mathematical	—	Finset.card support Equiv.Perm instMul Equiv.swap DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike	—	Finset.card_lt_card mem_support_swap_mul_imp_mem_support_ne mem_support Equiv.swap_apply_right
coe_support_eq_set_support 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike support setOf DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	Set.ext
disjoint_comm 📖	mathematical	—	Disjoint	—	Disjoint.symm
disjoint_conj 📖	mathematical	—	Disjoint Equiv.Perm instMul instInv	—	Equiv.forall_congr
disjoint_iff_disjoint_support 📖	mathematical	—	Disjoint Disjoint Finset Finset.partialOrder Finset.instOrderBot support	—	—
disjoint_iff_eq_or_eq 📖	mathematical	—	Disjoint DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	—
disjoint_inv_left_iff 📖	mathematical	—	Disjoint Equiv.Perm instInv	—	Disjoint.inv_left
disjoint_inv_right_iff 📖	mathematical	—	Disjoint Equiv.Perm instInv	—	disjoint_comm disjoint_inv_left_iff
disjoint_noncommProd_right 📖	mathematical	Set.Pairwise SetLike.coe Finset Finset.instSetLike Commute Equiv.Perm instMul Disjoint	Finset.noncommProd DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup	—	Finset.noncommProd_induction Disjoint.mul_right disjoint_one_right
disjoint_one_left 📖	mathematical	—	Disjoint Equiv.Perm instOne	—	—
disjoint_one_right 📖	mathematical	—	Disjoint Equiv.Perm instOne	—	—
disjoint_prod_perm 📖	mathematical	Equiv.Perm Disjoint	instMul instOne	—	List.Perm.prod_eq' Disjoint.commute
disjoint_prod_right 📖	mathematical	Disjoint	Equiv.Perm instMul instOne	—	disjoint_one_right Disjoint.mul_right
disjoint_refl_iff 📖	mathematical	—	Disjoint Equiv.Perm instOne	—	ext disjoint_one_left
disjoint_swap_swap 📖	mathematical	—	Disjoint Equiv.swap	—	—
eq_on_support_mem_disjoint 📖	mathematical	Equiv.Perm Disjoint Finset Finset.instMembership support	DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike instMul instOne	—	mul_apply notMem_support Disjoint.mem_imp disjoint_prod_right Disjoint.symm EquivLike.toEmbeddingLike
exists_mem_support_of_mem_support_prod 📖	—	Finset Finset.instMembership support Equiv.Perm instMul instOne	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq mul_apply
fixed_point_card_lt_of_ne_one 📖	mathematical	—	Finset.card Finset.filter DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Finset.univ Fintype.card	—	Finset.card_compl Finset.compl_filter one_lt_card_support_of_ne_one
instSymmDisjoint 📖	mathematical	—	Equiv.Perm Disjoint	—	Disjoint.symmetric
isInvariant_of_support_le 📖	mathematical	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder support	Finset.instMembership DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	apply_mem_support notMem_support
mem_support 📖	mathematical	—	Finset Finset.instMembership support	—	support.eq_1 Finset.mem_filter Finset.mem_univ
mem_support_iff_of_commute 📖	mathematical	Commute Equiv.Perm instMul	Finset Finset.instMembership support DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike	—	mul_apply Equiv.apply_eq_iff_eq
mem_support_of_mem_noncommProd_support 📖	—	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Equiv.Perm Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Finset.instMembership support Finset.noncommProd	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Finset.induction Finset.coe_empty instIsEmptyFalse support_one Set.Pairwise.mono Finset.mem_insert_of_mem Finset.noncommProd_insert_of_notMem Finset.mem_of_subset support_mul_le Finset.sup_eq_union Finset.notMem_union Finset.mem_insert_self
mem_support_swap_mul_imp_mem_support_ne 📖	—	Finset Finset.instMembership support Equiv.Perm instMul Equiv.swap DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike	—	—	Equiv.injective
ne_and_ne_of_swap_mul_apply_ne_self 📖	—	—	—	—	Equiv.injective
nodup_of_pairwise_disjoint 📖	—	Equiv.Perm instOne Disjoint	—	—	ext
notMem_support 📖	mathematical	—	Finset Finset.instMembership support DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	—
ofSubtype_eq_iff 📖	mathematical	Finset Finset.instMembership DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup MonoidHom.instFunLike ofSubtype Finset.decidableMem subtypePerm Preorder.toLE PartialOrder.toPreorder Finset.partialOrder support	—	ofSubtype_apply_of_not_mem mem_support ofSubtype_apply_of_mem subtypePerm_apply isInvariant_of_support_le notMem_support Finset.notMem_mono
ofSubtype_swap_eq 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup MonoidHom.instFunLike ofSubtype Equiv.swap	—	Equiv.ext Equiv.swap_apply_def ofSubtype_apply_of_mem Subtype.coe_eta Equiv.swap_apply_left Equiv.swap_apply_right Equiv.swap_apply_of_ne_of_ne ofSubtype_apply_of_not_mem
one_lt_card_support_of_ne_one 📖	mathematical	—	Finset.card support	—	Mathlib.Tactic.Contrapose.contrapose₂ ext Equiv.apply_eq_iff_eq
pow_apply_eq_of_apply_apply_eq_self 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	instPowNat	—	pow_succ' mul_apply
pow_apply_eq_self_of_apply_eq_self 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	instPowNat	—	pow_succ mul_apply
pow_apply_mem_support 📖	mathematical	—	Finset Finset.instMembership support DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instPowNat	—	—
pow_eq_on_of_mem_support 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Finset Finset.instMembership Finset.instInter support	instPowNat	—	pow_zero pow_succ mul_apply Finset.mem_inter apply_mem_support
set_support_apply_mem 📖	mathematical	—	Set Set.instMembership setOf DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	EquivLike.toEmbeddingLike
set_support_inv_eq 📖	mathematical	—	setOf DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.Perm	—	set_support_symm_eq
set_support_mul_subset 📖	mathematical	—	Set Set.instHasSubset setOf DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instMul Set.instUnion	—	—
set_support_symm_eq 📖	mathematical	—	setOf DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.Perm	—	Set.ext
set_support_zpow_subset 📖	mathematical	—	Set Set.instHasSubset setOf DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike DivInvMonoid.toZPow Group.toDivInvMonoid permGroup	—	zpow_apply_eq_self_of_apply_eq_self
support_congr 📖	—	Finset Finset.instHasSubset support DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	—	—
support_conj 📖	mathematical	—	support Equiv.Perm instMul instInv Finset.map Equiv.toEmbedding	—	Finset.ext
support_eq_empty_iff 📖	mathematical	—	support Finset Finset.instEmptyCollection Equiv.Perm instOne	—	—
support_extend_domain 📖	mathematical	—	support extendDomain Finset.map Equiv.asEmbedding	—	Finset.ext extendDomain_apply_subtype extendDomain_apply_not_subtype Subtype.prop
support_inv 📖	mathematical	—	support Equiv.Perm instInv	—	inv_eq_iff_eq
support_le_prod_of_mem 📖	mathematical	Equiv.Perm Disjoint	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder support instMul instOne	—	mem_support eq_on_support_mem_disjoint
support_mul_le 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder support Equiv.Perm instMul SemilatticeSup.toMax Lattice.toSemilatticeSup Finset.instLattice	—	Finset.mem_union mem_support mul_apply not_and_or not_imp_not
support_noncommProd 📖	mathematical	Set.Pairwise SetLike.coe Finset Finset.instSetLike Disjoint	support Finset.noncommProd Equiv.Perm DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Set.Pairwise.imp Commute instMul Disjoint.commute Finset.biUnion	—	Finset.induction_on Set.Pairwise.imp Disjoint.commute support_one Set.Pairwise.mono Finset.coe_insert Finset.mem_insert_of_mem Finset.noncommProd_insert_of_notMem Finset.biUnion_insert Disjoint.support_mul disjoint_noncommProd_right
support_ofSubtype 📖	mathematical	—	support DFunLike.coe MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup MonoidHom.instFunLike ofSubtype Finset.map Function.Embedding.subtype Subtype.fintype	—	Finset.ext ofSubtype_apply_of_mem ofSubtype_apply_of_not_mem
support_one 📖	mathematical	—	support Equiv.Perm instOne Finset Finset.instEmptyCollection	—	support_eq_empty_iff
support_pow_le 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder support Equiv.Perm instPowNat	—	mem_support pow_apply_eq_self_of_apply_eq_self
support_prod_le 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder support Equiv.Perm instMul instOne SemilatticeSup.toMax Lattice.toSemilatticeSup Finset.instLattice Bot.bot BooleanAlgebra.toBot Finset.booleanAlgebra	—	support_one LE.le.trans support_mul_le sup_le_sup le_rfl
support_prod_of_pairwise_disjoint 📖	mathematical	Equiv.Perm Disjoint	support instMul instOne Finset SemilatticeSup.toMax Lattice.toSemilatticeSup Finset.instLattice Bot.bot BooleanAlgebra.toBot Finset.booleanAlgebra	—	support_one disjoint_prod_right Disjoint.support_mul
support_refl 📖	mathematical	—	support Equiv.refl Finset Finset.instEmptyCollection	—	support_one
support_subtypePerm 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	support Finset.Subtype.fintype subtypePerm Finset.filter Finset.univ	—	Finset.ext
support_swap 📖	mathematical	—	support Equiv.swap Finset Finset.instInsert Finset.instSingleton	—	Finset.ext Equiv.swap_apply_left Equiv.swap_apply_right Equiv.swap_apply_of_ne_of_ne
support_swap_iff 📖	mathematical	—	support Equiv.swap Finset Finset.instInsert Finset.instSingleton	—	Equiv.swap_self support_refl Finset.insert_eq_of_mem support_swap
support_swap_mul_eq 📖	mathematical	—	support Equiv.Perm instMul Equiv.swap DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike Finset Finset.instSDiff Finset.instSingleton	—	Equiv.swap_self Finset.sdiff_singleton_eq_erase Finset.erase_eq_of_notMem notMem_support Finset.ext Equiv.swap_apply_right Equiv.swap_apply_of_ne_of_ne EquivLike.toEmbeddingLike Equiv.swap_apply_left Equiv.injective
support_swap_mul_ge_support_diff 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Finset.instSDiff support Finset.instInsert Finset.instSingleton Equiv.Perm instMul Equiv.swap	—	Equiv.swap_apply_of_ne_of_ne Equiv.swap_apply_eq_iff
support_swap_mul_swap 📖	mathematical	—	support Equiv.Perm instMul Equiv.swap Finset Finset.instInsert Finset.instSingleton	—	le_antisymm support_swap Finset.union_insert Finset.insert_union Finset.insert_eq_of_mem support_mul_le Equiv.swap_apply_of_ne_of_ne Equiv.swap_apply_left Equiv.swap_apply_right
support_zpow_le 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder support Equiv.Perm DivInvMonoid.toZPow Group.toDivInvMonoid permGroup	—	mem_support zpow_apply_eq_self_of_apply_eq_self
two_le_card_support_of_ne_one 📖	mathematical	—	Finset.card support	—	one_lt_card_support_of_ne_one
zpow_apply_eq_of_apply_apply_eq_self 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	DivInvMonoid.toZPow Group.toDivInvMonoid permGroup	—	pow_apply_eq_of_apply_apply_eq_self zpow_negSucc inv_eq_iff_eq Equiv.injective mul_apply pow_succ' pow_succ
zpow_apply_eq_self_of_apply_eq_self 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	DivInvMonoid.toZPow Group.toDivInvMonoid permGroup	—	pow_apply_eq_self_of_apply_eq_self zpow_negSucc inv_eq_iff_eq
zpow_apply_mem_support 📖	mathematical	—	Finset Finset.instMembership support DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike DivInvMonoid.toZPow Group.toDivInvMonoid permGroup	—	—

Equiv.Perm.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_support_mul 📖	mathematical	Equiv.Perm.Disjoint	Finset.card Equiv.Perm.support Equiv.Perm Equiv.Perm.instMul	—	Finset.card_union_of_disjoint disjoint_support Finset.ext support_mul
commute 📖	mathematical	Equiv.Perm.Disjoint	Commute Equiv.Perm Equiv.Perm.instMul	—	Equiv.ext Equiv.injective
conj 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm Equiv.Perm.instMul Equiv.Perm.instInv	—	Equiv.Perm.disjoint_conj
disjoint_support 📖	mathematical	Equiv.Perm.Disjoint	Disjoint Finset Finset.partialOrder Finset.instOrderBot Equiv.Perm.support	—	Equiv.Perm.disjoint_iff_disjoint_support
inv_left 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm Equiv.Perm.instInv	—	Equiv.Perm.inv_eq_iff_eq
inv_right 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm Equiv.Perm.instInv	—	symm inv_left
mem_imp 📖	—	Equiv.Perm.Disjoint Finset Finset.instMembership Equiv.Perm.support	—	—	Finset.disjoint_left disjoint_support
mono 📖	—	Equiv.Perm.Disjoint Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Equiv.Perm.support	—	—	Equiv.Perm.disjoint_iff_disjoint_support Disjoint.mono
mul_apply_eq_iff 📖	mathematical	Equiv.Perm.Disjoint	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instMul	—	Equiv.injective Equiv.Perm.mul_apply
mul_eq_one_iff 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm Equiv.Perm.instMul Equiv.Perm.instOne	—	mul_apply_eq_iff
mul_left 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm Equiv.Perm.instMul	—	—
mul_right 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm Equiv.Perm.instMul	—	Equiv.Perm.disjoint_comm mul_left symm
pow_disjoint_pow 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm Equiv.Perm.instPowNat	—	zpow_disjoint_zpow
support_mul 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm.support Equiv.Perm Equiv.Perm.instMul Finset Finset.instUnion	—	le_antisymm Equiv.Perm.support_mul_le Finset.mem_union Equiv.Perm.mem_support Equiv.Perm.mul_apply not_and_or not_imp_not Equiv.apply_eq_iff_eq
symmetric 📖	mathematical	—	Symmetric Equiv.Perm Equiv.Perm.Disjoint	—	symm
zpow_disjoint_zpow 📖	mathematical	Equiv.Perm.Disjoint	Equiv.Perm DivInvMonoid.toZPow Group.toDivInvMonoid Equiv.Perm.permGroup	—	Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self

Equiv.Perm.IsSwap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_subtype_isSwap 📖	mathematical	Equiv.Perm.IsSwap	DFunLike.coe MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup MonoidHom.instFunLike Equiv.Perm.ofSubtype	—	Equiv.Perm.ofSubtype_swap_eq

---

← Back to Index