Theorems · Theorem · group theory
Equiv.Perm.mem_cycleFactorsFinset_iff
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f p : Equiv.Perm α},
p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a- Defined in
- Mathlib.GroupTheory.Perm.Cycle.Factors
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqFintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- Equiv.Permstatement and proof · cited by 1,375
- Equiv.Perm.supportstatement and proof · cited by 230
- Equiv.Perm.IsCyclestatement and proof · cited by 108
- List.toFinsetproof · cited by 108
- Equiv.Perm.cycleFactorsFinsetstatement and proof · cited by 96
- Finset.exists_list_nodup_eqproof · cited by 2
- Equiv.Perm.mem_list_cycles_iffproof · cited by 2
- Equiv.Perm.cycleFactorsFinset_eq_list_toFinsetproof · cited by 1
Cited by17
Results whose statement or proof uses this declaration.
- Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iffproof · cited by 7
- Equiv.Perm.mem_cycleFactorsFinset_support_leproof · cited by 7
- Equiv.Perm.cycle_is_cycleOfproof · cited by 4
- Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinsetproof · cited by 3
- Equiv.Perm.Basis.nonemptyproof · cited by 2
- Equiv.Perm.OnCycleFactors.odd_of_centralizer_le_alternatingGroupproof · cited by 2
- Equiv.Perm.isConj_of_cycleType_eqproof · cited by 1
- Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinsetproof · cited by 1
- Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinsetproof · cited by 1
- Equiv.Perm.OnCycleFactors.kerParam_range_cardproof · cited by 1
- Equiv.Perm.Basis.toCentralizer_equivariantproof · cited by 1
- Equiv.Perm.subtypePerm_on_cycleFactorsFinsetproof · cited by 1