Factors

📁 Source: Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Statistics

Metric	Count
Definitions `cycleFactors`, `cycleFactorsAux`, `go`, `cycleFactorsFinset`, `cycleOf`, `instDecidableRelSameCycle`, `truncCycleFactors`	7
Theorems `cycleFactorsFinset_mul_eq_union`, `cycleOf_mul_distrib`, `disjoint_cycleFactorsFinset`, `cycleFactorsFinset_eq_singleton`, `cycleOf`, `cycleOf_eq`, `forall_commute_iff`, `cycleOf_apply`, `cycleOf_eq`, `exists_pow_eq`, `exists_pow_eq_of_mem_support`, `mem_support_iff`, `commute_iff_of_mem_cycleFactorsFinset`, `commute_ofSubtype_noncommPiCoprod`, `commute_of_mem_cycleFactorsFinset_commute`, `cycleFactorsFinset_eq_empty_iff`, `cycleFactorsFinset_eq_finset`, `cycleFactorsFinset_eq_list_toFinset`, `cycleFactorsFinset_eq_singleton_iff`, `cycleFactorsFinset_eq_singleton_self_iff`, `cycleFactorsFinset_injective`, `cycleFactorsFinset_mem_commute`, `cycleFactorsFinset_mem_commute'`, `cycleFactorsFinset_mul_inv_mem_eq_sdiff`, `cycleFactorsFinset_noncommProd`, `cycleFactorsFinset_one`, `cycleFactorsFinset_pairwise_disjoint`, `cycleOf_apply`, `cycleOf_apply_apply_pow_self`, `cycleOf_apply_apply_self`, `cycleOf_apply_apply_zpow_self`, `cycleOf_apply_of_not_sameCycle`, `cycleOf_apply_self`, `cycleOf_eq_one_iff`, `cycleOf_inv`, `cycleOf_mem_cycleFactorsFinset_iff`, `cycleOf_mul_of_apply_right_eq_self`, `cycleOf_ne_one_iff_mem_cycleFactorsFinset`, `cycleOf_one`, `cycleOf_pow_apply_self`, `cycleOf_self_apply`, `cycleOf_self_apply_pow`, `cycleOf_self_apply_zpow`, `cycleOf_zpow_apply_self`, `cycle_induction_on`, `cycle_is_cycleOf`, `disjoint_mul_inv_of_mem_cycleFactorsFinset`, `disjoint_ofSubtype_noncommPiCoprod`, `eq_cycleOf_of_mem_cycleFactorsFinset_iff`, `isCycleOn_support_cycleOf`, `isCycleOn_support_of_mem_cycleFactorsFinset`, `isCycle_cycleOf`, `isCycle_cycleOf_iff`, `list_cycles_perm_list_cycles`, `mem_cycleFactorsFinset_conj`, `mem_cycleFactorsFinset_iff`, `mem_cycleFactorsFinset_support`, `mem_cycleFactorsFinset_support_le`, `mem_list_cycles_iff`, `mem_support_cycleOf_iff`, `mem_support_cycleOf_iff'`, `mem_support_cycle_of_cycle`, `mem_support_iff_mem_support_of_mem_cycleFactorsFinset`, `pairwise_commute_of_mem_zpowers`, `pairwise_disjoint_of_mem_zpowers`, `pow_mod_card_support_cycleOf_self_apply`, `pow_mod_orderOf_cycleOf_apply`, `sameCycle_iff_cycleOf_eq_of_mem_support`, `self_mem_cycle_factors_commute`, `subtypePerm_on_cycleFactorsFinset`, `support_cycleOf_eq_nil_iff`, `support_cycleOf_le`, `support_cycleOf_nonempty`, `support_zpowers_of_mem_cycleFactorsFinset_le`, `two_le_card_support_cycleOf_iff`, `zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff`, `zpow_eq_zpow_on_iff`	77
Total	84

Equiv.Perm

Definitions

Name	Category	Theorems
`cycleFactors` 📖	CompOp	—
`cycleFactorsAux` 📖	CompOp	—
`cycleFactorsFinset` 📖	CompOp	61 math math: `mem_cycleFactorsFinset_conj`, `Basis.injective`, `Basis.toCentralizer_equivariant`, `cycleFactorsFinset_eq_empty_iff`, `Basis.toCentralizer_apply`, `disjoint_ofSubtype_noncommPiCoprod`, `OnCycleFactors.mem_range_toPermHom_iff'`, `Basis.mem_support_self'`, `OnCycleFactors.kerParam_range_card`, `OnCycleFactors.kerParam_injective`, `OnCycleFactors.nat_card_range_toPermHom`, `zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff`, `cycleFactorsFinset_eq_finset`, `IsCycle.cycleFactorsFinset_eq_singleton`, `cycleFactorsFinset_eq_singleton_self_iff`, `Disjoint.disjoint_cycleFactorsFinset`, `Basis.card_ofPermHom_support`, `Basis.ofPermHom_apply`, `mem_support_iff_mem_support_of_mem_cycleFactorsFinset`, `OnCycleFactors.mem_range_toPermHom'_iff`, `cycleFactorsFinset_one`, `Basis.ofPermHom_mem_centralizer`, `support_zpowers_of_mem_cycleFactorsFinset_le`, `Basis.mem_support_self`, `OnCycleFactors.val_centralizer_smul`, `cycleFactorsFinset_eq_singleton_iff`, `Basis.toPermHom_apply_toCentralizer`, `OnCycleFactors.mem_ker_toPermHom_iff`, `Basis.ofPermHom_support`, `cycleFactorsFinset_pairwise_disjoint`, `pairwise_commute_of_mem_zpowers`, `Basis.ofPermHomFun_apply_mem_support_cycle_iff`, `mem_cycleFactorsFinset_conj'`, `OnCycleFactors.cycleType_kerParam_apply_apply`, `OnCycleFactors.coe_toPermHom`, `cycleFactorsFinset_conj_eq`, `OnCycleFactors.mem_range_toPermHom_iff`, `OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one`, `cycleOf_mem_cycleFactorsFinset_iff`, `mem_cycleFactorsFinset_iff`, `Basis.mem_fixedPoints_or_exists_zpow_eq`, `cycleFactorsFinset_mem_commute`, `OnCycleFactors.toPermHom_apply`, `cycleFactorsFinset_eq_list_toFinset`, `cycleFactorsFinset_conj`, `Basis.ofPermHomFun_mul`, `cycleType_def`, `Basis.cycleOf_eq`, `OnCycleFactors.kerParam_range_le_centralizer`, `pairwise_disjoint_of_mem_zpowers`, `CycleType.count_def`, `Disjoint.cycleFactorsFinset_mul_eq_union`, `cycleFactorsFinset_injective`, `OnCycleFactors.kerParam_range_eq`, `Basis.ofPermHomFun_one`, `OnCycleFactors.kerParam_apply`, `cycleOf_ne_one_iff_mem_cycleFactorsFinset`, `OnCycleFactors.range_toPermHom_eq_range_toPermHom'`, `OnCycleFactors.centralizer_smul_def`, `commute_ofSubtype_noncommPiCoprod`, `OnCycleFactors.sign_kerParam_apply_apply`
`cycleOf` 📖	CompOp	45 math math: `SameCycle.exists_pow_eq_of_mem_support`, `isCycle_cycleOf_iff`, `SameCycle.exists_pow_eq`, `cycleOf_inv`, `isCycle_cycleOf`, `cycleOf_self_apply_zpow`, `support_cycleOf_le`, `cycleOf_eq_one_iff`, `support_cycleOf_nonempty`, `cycleOf_one`, `isCycleOn_support_cycleOf`, `cycleOf_apply_apply_pow_self`, `mem_support_cycleOf_iff`, `cycleOf_pow_apply_self`, `SameCycle.cycleOf_eq`, `cycle_is_cycleOf`, `mem_support_cycleOf_iff'`, `cycleOf_apply_apply_self`, `cycleOf_self_apply_pow`, `cycleOf_apply_apply_zpow_self`, `support_cycleOf_eq_nil_iff`, `cycleOf_apply_of_not_sameCycle`, `IsCycle.cycleOf_eq`, `formPerm_toList`, `IsCycle.cycleOf`, `zpow_eq_zpow_on_iff`, `cycleOf_self_apply`, `cycleOf_apply`, `pow_mod_card_support_cycleOf_self_apply`, `cycleOf_mem_cycleFactorsFinset_iff`, `sameCycle_iff_cycleOf_eq_of_mem_support`, `two_le_card_support_cycleOf_iff`, `SameCycle.cycleOf_apply`, `length_toList`, `eq_cycleOf_of_mem_cycleFactorsFinset_iff`, `Basis.cycleOf_eq`, `orderOf_cycleOf_dvd_orderOf`, `cycleOf_mul_of_apply_right_eq_self`, `List.cycleOf_formPerm`, `pow_mod_orderOf_cycleOf_apply`, `cycleOf_zpow_apply_self`, `cycleOf_apply_self`, `OnCycleFactors.kerParam_apply`, `Disjoint.cycleOf_mul_distrib`, `cycleOf_ne_one_iff_mem_cycleFactorsFinset`
`instDecidableRelSameCycle` 📖	CompOp	22 math math: `SameCycle.exists_pow_eq_of_mem_support`, `SameCycle.exists_pow_eq`, `support_cycleOf_le`, `support_cycleOf_nonempty`, `isCycleOn_support_cycleOf`, `mem_support_cycleOf_iff`, `cycle_is_cycleOf`, `mem_support_cycleOf_iff'`, `support_cycleOf_eq_nil_iff`, `formPerm_toList`, `zpow_eq_zpow_on_iff`, `pow_mod_card_support_cycleOf_self_apply`, `cycleOf_mem_cycleFactorsFinset_iff`, `sameCycle_iff_cycleOf_eq_of_mem_support`, `two_le_card_support_cycleOf_iff`, `length_toList`, `eq_cycleOf_of_mem_cycleFactorsFinset_iff`, `Basis.cycleOf_eq`, `orderOf_cycleOf_dvd_orderOf`, `List.cycleOf_formPerm`, `OnCycleFactors.kerParam_apply`, `cycleOf_ne_one_iff_mem_cycleFactorsFinset`
`truncCycleFactors` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_iff_of_mem_cycleFactorsFinset` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`Commute` `instMul` `support` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `subtypePerm` `mem_cycleFactorsFinset_support`	—	`mem_cycleFactorsFinset_support` `IsCycle.commute_iff'` `mem_cycleFactorsFinset_iff` `subtypePerm_on_cycleFactorsFinset`
`commute_ofSubtype_noncommPiCoprod` 📖	mathematical	—	`Commute` `Equiv.Perm` `instMul` `DFunLike.coe` `MonoidHom` `Set` `Set.instMembership` `Function.fixedPoints` `EquivLike.toFunLike` `Equiv.instEquivLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MonoidHom.instFunLike` `ofSubtype` `Function.fixedPoints.decidable` `Pi.mulOneClass` `Finset` `SetLike.instMembership` `Finset.instSetLike` `cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `Subgroup.noncommPiCoprod` `Finset.Subtype.fintype` `pairwise_commute_of_mem_zpowers`	—	`Disjoint.commute` `pairwise_commute_of_mem_zpowers` `disjoint_ofSubtype_noncommPiCoprod`
`commute_of_mem_cycleFactorsFinset_commute` 📖	—	`Commute` `Equiv.Perm` `instMul`	—	—	`cycleFactorsFinset_mem_commute` `cycleFactorsFinset_noncommProd` `Finset.noncommProd_commute`
`cycleFactorsFinset_eq_empty_iff` 📖	mathematical	—	`cycleFactorsFinset` `Finset` `Equiv.Perm` `Finset.instEmptyCollection` `instOne`	—	`Set.Pairwise.mono'` `Disjoint.commute` `instIsEmptyFalse` `Finset.noncommProd_congr` `Finset.coe_empty`
`cycleFactorsFinset_eq_finset` 📖	mathematical	—	`cycleFactorsFinset` `IsCycle` `Finset.noncommProd` `Equiv.Perm` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Set.Pairwise.mono'` `Disjoint` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SetLike.coe` `Finset` `Finset.instSetLike` `Disjoint.commute`	—	`Set.Pairwise.mono'` `Disjoint.commute` `Finset.exists_list_nodup_eq` `Finset.noncommProd_congr` `Finset.noncommProd_toFinset` `List.coe_toFinset` `instSymmDisjoint`
`cycleFactorsFinset_eq_list_toFinset` 📖	mathematical	`Equiv.Perm`	`cycleFactorsFinset` `List.toFinset` `Fintype.decidableEqEquivFintype` `IsCycle` `Disjoint` `instMul` `instOne`	—	`Trunc.exists_rep` `cycleFactorsFinset.eq_1` `Multiset.toFinset_eq` `List.toFinset_coe` `nodup_of_pairwise_disjoint_cycles` `List.perm_of_nodup_nodup_toFinset_eq` `Disjoint.symmetric` `List.Perm.prod_eq'` `Disjoint.commute` `List.toFinset_eq_of_perm` `list_cycles_perm_list_cycles` `Finite.of_fintype`
`cycleFactorsFinset_eq_singleton_iff` 📖	mathematical	—	`cycleFactorsFinset` `Equiv.Perm` `Finset` `Finset.instSingleton` `IsCycle`	—	`Set.Pairwise.mono'` `Disjoint.commute` `cycleFactorsFinset_eq_finset` `Finset.noncommProd_congr` `Finset.noncommProd_singleton` `Finset.coe_singleton`
`cycleFactorsFinset_eq_singleton_self_iff` 📖	mathematical	—	`cycleFactorsFinset` `Equiv.Perm` `Finset` `Finset.instSingleton` `IsCycle`	—	`Set.Pairwise.mono'` `Disjoint.commute` `Finset.noncommProd_congr` `Finset.noncommProd_singleton` `Finset.coe_singleton`
`cycleFactorsFinset_injective` 📖	mathematical	—	`Equiv.Perm` `Finset` `cycleFactorsFinset`	—	`cycleFactorsFinset_mem_commute` `cycleFactorsFinset_noncommProd` `Finset.noncommProd_congr`
`cycleFactorsFinset_mem_commute` 📖	mathematical	—	`Set.Pairwise` `Equiv.Perm` `SetLike.coe` `Finset` `Finset.instSetLike` `cycleFactorsFinset` `Commute` `instMul`	—	`Set.Pairwise.mono'` `Disjoint.commute` `cycleFactorsFinset_pairwise_disjoint`
`cycleFactorsFinset_mem_commute'` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`Commute` `instMul`	—	`eq_or_ne` `Commute.refl` `cycleFactorsFinset_mem_commute`
`cycleFactorsFinset_mul_inv_mem_eq_sdiff` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`instMul` `instInv` `Finset.instSDiff` `Fintype.decidableEqEquivFintype` `Finset.instSingleton`	—	`cycle_induction_on` `Finite.of_fintype` `cycleFactorsFinset_one` `one_mul` `Finset.empty_sdiff` `instIsEmptyFalse` `cycleFactorsFinset_eq_singleton_self_iff` `mul_inv_cancel` `sdiff_self` `Disjoint.cycleFactorsFinset_mul_eq_union` `Commute.eq` `Disjoint.commute` `Finset.union_comm` `Finset.union_sdiff_distrib` `Finset.sdiff_singleton_eq_erase` `Finset.erase_eq_of_notMem` `Finset.notMem_empty` `Disjoint.le_bot` `Disjoint.disjoint_cycleFactorsFinset` `Finset.mem_inter_of_mem` `mul_assoc` `Disjoint.symm` `Equiv.symm_apply_apply` `mul_apply` `mem_cycleFactorsFinset_iff` `mem_support`
`cycleFactorsFinset_noncommProd` 📖	mathematical	`Set.Pairwise` `Equiv.Perm` `SetLike.coe` `Finset` `Finset.instSetLike` `cycleFactorsFinset` `Commute` `instMul` `cycleFactorsFinset_mem_commute`	`Finset.noncommProd` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup`	—	`Set.Pairwise.mono'` `Disjoint.commute` `cycleFactorsFinset_eq_finset`
`cycleFactorsFinset_one` 📖	mathematical	—	`cycleFactorsFinset` `Equiv.Perm` `instOne` `Finset` `Finset.instEmptyCollection`	—	—
`cycleFactorsFinset_pairwise_disjoint` 📖	mathematical	—	`Set.Pairwise` `Equiv.Perm` `SetLike.coe` `Finset` `Finset.instSetLike` `cycleFactorsFinset` `Disjoint`	—	`Set.Pairwise.mono'` `Disjoint.commute` `cycleFactorsFinset_eq_finset`
`cycleOf_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleOf` `SameCycle`	—	`sameCycle_apply_right` `ofSubtype_apply_of_mem` `ofSubtype_apply_of_not_mem`
`cycleOf_apply_apply_pow_self` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleOf` `instPowNat`	—	`cycleOf_apply_apply_zpow_self`
`cycleOf_apply_apply_self` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleOf`	—	`cycleOf_apply_apply_pow_self`
`cycleOf_apply_apply_zpow_self` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleOf` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `permGroup`	—	`SameCycle.cycleOf_apply` `add_comm` `zpow_add` `zpow_one` `mul_apply`
`cycleOf_apply_of_not_sameCycle` 📖	mathematical	`SameCycle`	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleOf`	—	`ofSubtype_apply_of_not_mem` `sameCycle_apply_right`
`cycleOf_apply_self` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleOf`	—	`SameCycle.cycleOf_apply` `SameCycle.rfl`
`cycleOf_eq_one_iff` 📖	mathematical	—	`cycleOf` `Equiv.Perm` `instOne` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`cycleOf_apply` `SameCycle.refl` `SameCycle.apply_eq_self_iff`
`cycleOf_inv` 📖	mathematical	—	`Equiv.Perm` `instInv` `cycleOf` `instDecidableRelSameCycleInv`	—	`Equiv.ext` `inv_eq_iff_eq` `cycleOf_apply` `Equiv.apply_symm_apply`
`cycleOf_mem_cycleFactorsFinset_iff` 📖	mathematical	—	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset` `cycleOf` `instDecidableRelSameCycle` `support`	—	`mem_cycleFactorsFinset_iff` `Mathlib.Tactic.Contrapose.contrapose₁` `cycleOf_eq_one_iff` `notMem_support` `isCycle_cycleOf` `mem_support` `cycleOf_apply` `cycleOf_apply_of_not_sameCycle`
`cycleOf_mul_of_apply_right_eq_self` 📖	mathematical	`Commute` `Equiv.Perm` `instMul` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	`cycleOf`	—	`ext` `cycleOf_apply_apply_zpow_self` `Commute.mul_zpow` `zpow_apply_eq_self_of_apply_eq_self` `cycleOf_apply_of_not_sameCycle` `Mathlib.Tactic.Contrapose.contrapose₄`
`cycleOf_ne_one_iff_mem_cycleFactorsFinset` 📖	mathematical	—	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset` `cycleOf` `instDecidableRelSameCycle`	—	`cycleOf_mem_cycleFactorsFinset_iff` `mem_support` `cycleOf_eq_one_iff`
`cycleOf_one` 📖	mathematical	—	`cycleOf` `Equiv.Perm` `instOne`	—	`cycleOf_eq_one_iff`
`cycleOf_pow_apply_self` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `instPowNat` `cycleOf`	—	`pow_succ'` `mul_apply` `cycleOf_apply`
`cycleOf_self_apply` 📖	mathematical	—	`cycleOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`SameCycle.cycleOf_eq` `SameCycle.symm` `sameCycle_apply_right` `SameCycle.rfl`
`cycleOf_self_apply_pow` 📖	mathematical	—	`cycleOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `instPowNat`	—	`SameCycle.cycleOf_eq` `SameCycle.pow_left` `SameCycle.rfl`
`cycleOf_self_apply_zpow` 📖	mathematical	—	`cycleOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `permGroup`	—	`SameCycle.cycleOf_eq` `SameCycle.zpow_left` `SameCycle.rfl`
`cycleOf_zpow_apply_self` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `permGroup` `cycleOf`	—	`cycleOf_pow_apply_self` `zpow_negSucc` `inv_pow` `cycleOf_inv`
`cycle_induction_on` 📖	—	`Equiv.Perm` `instOne` `instMul`	—	—	`nonempty_fintype` `disjoint_prod_right`
`cycle_is_cycleOf` 📖	mathematical	`Finset` `Finset.instMembership` `support` `Equiv.Perm` `cycleFactorsFinset`	`cycleOf` `instDecidableRelSameCycle`	—	`Disjoint.symm` `disjoint_mul_inv_of_mem_cycleFactorsFinset` `Disjoint.commute` `cycleOf_mul_of_apply_right_eq_self` `notMem_support` `Finset.disjoint_left` `Disjoint.disjoint_support` `cycleOf.congr_simp` `Commute.eq` `inv_mul_cancel_right` `symm` `IsEquiv.toSymm` `eq_isEquiv` `IsCycle.cycleOf_eq` `mem_cycleFactorsFinset_iff` `mem_support`
`disjoint_mul_inv_of_mem_cycleFactorsFinset` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`Disjoint` `instMul` `instInv`	—	`mul_apply` `mem_cycleFactorsFinset_iff` `Equiv.apply_symm_apply`
`disjoint_ofSubtype_noncommPiCoprod` 📖	mathematical	—	`Disjoint` `DFunLike.coe` `MonoidHom` `Equiv.Perm` `Set` `Set.instMembership` `Function.fixedPoints` `EquivLike.toFunLike` `Equiv.instEquivLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MonoidHom.instFunLike` `ofSubtype` `Function.fixedPoints.decidable` `Pi.mulOneClass` `Finset` `SetLike.instMembership` `Finset.instSetLike` `cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `Subgroup.noncommPiCoprod` `Finset.Subtype.fintype` `pairwise_commute_of_mem_zpowers`	—	`Finset.noncommProd_induction` `pairwise_commute_of_mem_zpowers` `Disjoint.mul_right` `disjoint_one_right` `Disjoint.mono` `disjoint_ofSubtype_of_memFixedPoints_self` `le_rfl` `support_zpowers_of_mem_cycleFactorsFinset_le`
`eq_cycleOf_of_mem_cycleFactorsFinset_iff` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`cycleOf` `instDecidableRelSameCycle` `support`	—	`mem_support` `cycleOf_apply_self` `cycleOf_eq_one_iff` `IsCycle.ne_one` `mem_cycleFactorsFinset_iff` `cycle_is_cycleOf`
`isCycleOn_support_cycleOf` 📖	mathematical	—	`IsCycleOn` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `cycleOf` `instDecidableRelSameCycle`	—	—
`isCycleOn_support_of_mem_cycleFactorsFinset` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`IsCycleOn` `SetLike.coe` `Finset.instSetLike` `support`	—	`IsCycle.nonempty_support` `mem_cycleFactorsFinset_iff` `cycle_is_cycleOf` `isCycleOn_support_cycleOf`
`isCycle_cycleOf` 📖	mathematical	—	`IsCycle` `cycleOf`	—	`SameCycle.cycleOf_apply` `SameCycle.rfl` `isCycle_iff_sameCycle` `SameCycle.apply_eq_self_iff` `cycleOf_zpow_apply_self` `cycleOf_apply_of_not_sameCycle`
`isCycle_cycleOf_iff` 📖	mathematical	—	`IsCycle` `cycleOf`	—	`cycleOf_eq_one_iff` `IsCycle.ne_one` `isCycle_cycleOf`
`list_cycles_perm_list_cycles` 📖	—	`Equiv.Perm` `instMul` `instOne` `IsCycle` `Disjoint`	—	—	`nodup_of_pairwise_disjoint_cycles` `mem_list_cycles_iff`
`mem_cycleFactorsFinset_conj` 📖	mathematical	—	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset` `instMul` `instInv`	—	`IsCycle.conj` `EquivLike.toEmbeddingLike` `support_conj` `neg_add_cancel` `zpow_zero` `one_mul` `Mathlib.Tactic.Group.zpow_trick_one'` `mul_one`
`mem_cycleFactorsFinset_iff` 📖	mathematical	—	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset` `IsCycle` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Finset.exists_list_nodup_eq` `cycleFactorsFinset_eq_list_toFinset` `mem_list_cycles_iff` `Finite.of_fintype`
`mem_cycleFactorsFinset_support` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`support` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`mem_support_iff_of_commute` `Commute.symm` `self_mem_cycle_factors_commute`
`mem_cycleFactorsFinset_support_le` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `support`	—	`mem_support` `mem_cycleFactorsFinset_iff`
`mem_list_cycles_iff` 📖	mathematical	`IsCycle` `Equiv.Perm` `Disjoint`	`DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `instMul` `instOne`	—	`nonempty_fintype` `eq_on_support_mem_disjoint` `mem_support` `exists_mem_support_of_mem_support_prod` `Finset.mem_of_mem_inter_left` `Finset.mem_of_mem_inter_right` `IsCycle.eq_on_support_inter_nonempty_congr` `Finset.mem_inter_of_mem`
`mem_support_cycleOf_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `cycleOf` `instDecidableRelSameCycle` `SameCycle`	—	—
`mem_support_cycleOf_iff'` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `cycleOf` `instDecidableRelSameCycle` `SameCycle`	—	—
`mem_support_cycle_of_cycle` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`support` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike` `mul_apply` `Commute.eq` `cycleFactorsFinset_mem_commute`
`mem_support_iff_mem_support_of_mem_cycleFactorsFinset` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `Equiv.Perm` `cycleFactorsFinset`	—	`cycleOf_mem_cycleFactorsFinset_iff` `mem_support_cycleOf_iff` `SameCycle.refl` `mem_cycleFactorsFinset_support_le`
`pairwise_commute_of_mem_zpowers` 📖	mathematical	—	`Pairwise` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `cycleFactorsFinset`	—	`Pairwise.mono` `pairwise_disjoint_of_mem_zpowers` `forall₂_imp` `Disjoint.commute`
`pairwise_disjoint_of_mem_zpowers` 📖	mathematical	—	`Pairwise` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `cycleFactorsFinset`	—	`Disjoint.zpow_disjoint_zpow` `cycleFactorsFinset_pairwise_disjoint` `Subtype.prop` `Subtype.coe_ne_coe`
`pow_mod_card_support_cycleOf_self_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `instPowNat` `Finset.card` `support` `cycleOf` `instDecidableRelSameCycle`	—	`pow_apply_eq_self_of_apply_eq_self` `cycleOf_pow_apply_self` `IsCycle.orderOf` `isCycle_cycleOf` `pow_mod_orderOf`
`pow_mod_orderOf_cycleOf_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `instPowNat` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `cycleOf`	—	`cycleOf_pow_apply_self` `pow_mod_orderOf`
`sameCycle_iff_cycleOf_eq_of_mem_support` 📖	mathematical	`Finset` `Finset.instMembership` `support`	`SameCycle` `cycleOf` `instDecidableRelSameCycle`	—	`SameCycle.cycleOf_eq` `mem_support_cycleOf_iff'` `mem_support` `SameCycle.refl`
`self_mem_cycle_factors_commute` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`Commute` `instMul`	—	`commute_of_mem_cycleFactorsFinset_commute` `Commute.refl` `cycleFactorsFinset_mem_commute`
`subtypePerm_on_cycleFactorsFinset` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `cycleFactorsFinset`	`subtypePerm` `support` `mem_cycleFactorsFinset_support` `subtypePermOfSupport`	—	`ext` `mem_cycleFactorsFinset_support` `mem_cycleFactorsFinset_iff`
`support_cycleOf_eq_nil_iff` 📖	mathematical	—	`support` `cycleOf` `instDecidableRelSameCycle` `Finset` `Finset.instEmptyCollection` `Finset.instMembership`	—	—
`support_cycleOf_le` 📖	mathematical	—	`Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `support` `cycleOf` `instDecidableRelSameCycle`	—	`mem_support` `cycleOf_apply`
`support_cycleOf_nonempty` 📖	mathematical	—	`Finset.Nonempty` `support` `cycleOf` `instDecidableRelSameCycle`	—	`two_le_card_support_cycleOf_iff` `Finset.card_pos` `LE.le.eq_or_lt` `card_support_ne_one` `LT.lt.trans_le` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`support_zpowers_of_mem_cycleFactorsFinset_le` 📖	mathematical	—	`Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `support` `Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Finset.instSetLike` `cycleFactorsFinset`	—	`Subtype.prop` `le_trans` `support_zpow_le` `mem_cycleFactorsFinset_support_le`
`two_le_card_support_cycleOf_iff` 📖	mathematical	—	`Finset.card` `support` `cycleOf` `instDecidableRelSameCycle`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `cycleOf_eq_one_iff` `support_one` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Nat.instAtLeastTwoHAddOfNat` `IsCycle.two_le_card_support` `isCycle_cycleOf`
`zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `Equiv.Perm` `SetLike.instMembership` `Finset.instSetLike` `cycleFactorsFinset` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `permGroup`	—	`eq_cycleOf_of_mem_cycleFactorsFinset_iff` `Subtype.prop` `cycleOf_self_apply_zpow`
`zpow_eq_zpow_on_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `permGroup` `Finset.card` `support` `cycleOf` `instDecidableRelSameCycle`	—	`zpow_add` `EquivLike.toEmbeddingLike` `cycleOf_zpow_apply_self` `cycle_zpow_mem_support_iff` `isCycle_cycleOf` `cycleOf_apply_self`

Equiv.Perm.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cycleFactorsFinset_mul_eq_union` 📖	mathematical	`Equiv.Perm.Disjoint`	`Equiv.Perm.cycleFactorsFinset` `Equiv.Perm` `Equiv.Perm.instMul` `Finset` `Finset.instUnion` `Fintype.decidableEqEquivFintype`	—	`Set.Pairwise.mono'` `commute` `Equiv.Perm.cycleFactorsFinset_eq_finset` `Finset.coe_union` `Set.pairwise_union_of_symmetric` `symmetric` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `mono` `Equiv.Perm.mem_cycleFactorsFinset_support_le` `Set.Pairwise.mono` `Finset.coe_subset` `Finset.subset_union_left` `Finset.subset_union_right` `Finset.noncommProd_union_of_disjoint` `disjoint_cycleFactorsFinset` `Equiv.Perm.cycleFactorsFinset_mem_commute` `Equiv.Perm.cycleFactorsFinset_noncommProd`
`cycleOf_mul_distrib` 📖	mathematical	`Equiv.Perm.Disjoint`	`Equiv.Perm.cycleOf` `Equiv.Perm` `Equiv.Perm.instMul`	—	`Equiv.Perm.disjoint_iff_eq_or_eq` `Equiv.Perm.cycleOf.congr_simp` `Commute.eq` `commute` `Equiv.Perm.cycleOf_mul_of_apply_right_eq_self` `symm` `RightCancelSemigroup.toIsRightCancelMul` `LeftCancelSemigroup.toIsLeftCancelMul`
`disjoint_cycleFactorsFinset` 📖	mathematical	`Equiv.Perm.Disjoint`	`Disjoint` `Finset` `Equiv.Perm` `Finset.partialOrder` `Finset.instOrderBot` `Equiv.Perm.cycleFactorsFinset`	—	`Finset.disjoint_left` `Disjoint.le_bot` `Equiv.Perm.disjoint_iff_disjoint_support`

Equiv.Perm.IsCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cycleFactorsFinset_eq_singleton` 📖	mathematical	`Equiv.Perm.IsCycle`	`Equiv.Perm.cycleFactorsFinset` `Equiv.Perm` `Finset` `Finset.instSingleton`	—	`Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff`
`cycleOf` 📖	mathematical	`Equiv.Perm.IsCycle`	`Equiv.Perm.cycleOf` `Equiv.Perm` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.Perm.instOne`	—	`Equiv.Perm.cycleOf_eq_one_iff` `cycleOf_eq`
`cycleOf_eq` 📖	mathematical	`Equiv.Perm.IsCycle`	`Equiv.Perm.cycleOf`	—	`Equiv.ext` `Equiv.Perm.SameCycle.cycleOf_apply` `Equiv.Perm.cycleOf_apply_of_not_sameCycle` `Equiv.Perm.isCycle_iff_sameCycle`
`forall_commute_iff` 📖	mathematical	—	`Commute` `Equiv.Perm` `Equiv.Perm.instMul` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `DFunLike.coe` `MonoidHom` `Finset` `Finset.instMembership` `Equiv.Perm.support` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Equiv.Perm.ofSubtype` `Finset.decidableMem` `Equiv.Perm.subtypePerm`	—	`commute_iff` `Equiv.Perm.mem_cycleFactorsFinset_iff`

Equiv.Perm.SameCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cycleOf_apply` 📖	mathematical	`Equiv.Perm.SameCycle`	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.Perm.cycleOf`	—	`Equiv.Perm.ofSubtype_apply_of_mem` `Equiv.Perm.sameCycle_apply_right`
`cycleOf_eq` 📖	mathematical	`Equiv.Perm.SameCycle`	`Equiv.Perm.cycleOf`	—	`Equiv.Perm.ext` `Equiv.Perm.cycleOf_apply` `cycleOf_apply` `trans` `symm` `Equiv.Perm.cycleOf_apply_of_not_sameCycle`
`exists_pow_eq` 📖	mathematical	`Equiv.Perm.SameCycle`	`Finset.card` `Equiv.Perm.support` `Equiv.Perm.cycleOf` `Equiv.Perm.instDecidableRelSameCycle` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.Perm.instPowNat`	—	`exists_pow_eq_of_mem_support` `self_le_add_right` `Nat.instCanonicallyOrderedAdd` `Equiv.Perm.IsCycle.orderOf` `Equiv.Perm.isCycle_cycleOf` `Equiv.Perm.mem_support` `Equiv.Perm.cycleOf_pow_apply_self` `pow_orderOf_eq_one` `Equiv.Perm.one_apply` `pow_zero` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `LT.lt.le` `zero_lt_one` `Nat.instZeroLEOneClass` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `Equiv.Perm.pow_apply_eq_self_of_apply_eq_self` `Equiv.Perm.notMem_support` `Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self`
`exists_pow_eq_of_mem_support` 📖	mathematical	`Equiv.Perm.SameCycle` `Finset` `Finset.instMembership` `Equiv.Perm.support`	`Finset.card` `Equiv.Perm.cycleOf` `Equiv.Perm.instDecidableRelSameCycle` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.Perm.instPowNat`	—	—
`mem_support_iff` 📖	mathematical	`Equiv.Perm.SameCycle`	`Finset` `Finset.instMembership` `Equiv.Perm.support`	—	`Equiv.Perm.support_cycleOf_le` `Equiv.Perm.mem_support_cycleOf_iff` `symm`

Equiv.Perm.cycleFactorsAux

Definitions

Name	Category	Theorems
`go` 📖	CompOp	—

---

← Back to Index