Theorems · Theorem · group theory

Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {τ : Equiv.Perm ↥g.cycleFactorsFinset},
  τ ∈ (Equiv.Perm.OnCycleFactors.toPermHom g).range ↔
    ∀ (c : ↥g.cycleFactorsFinset), (↑(τ c)).support.card = (↑c).support.card

Defined in: Mathlib.GroupTheory.Perm.Centralizer
Cited by: 3 results in Mathlib
Foundations: Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

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
Setstatement · cited by 53,352
Finsetstatement and proof · cited by 13,712
Fintypestatement and proof · cited by 7,736
Subgroupstatement · cited by 3,593
Finset.cardstatement and proof · cited by 2,327
Equiv.Permstatement and proof · cited by 1,375
MonoidHom.rangestatement and proof · cited by 314
Equiv.toEmbeddingproof · cited by 254
Equiv.Perm.supportstatement and proof · cited by 230
Finset.card_mapproof · cited by 114
Equiv.Perm.cycleFactorsFinsetstatement and proof · cited by 96

Cited by3

Results whose statement or proof uses this declaration.

Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff'proof · cited by 1
Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_oneproof · cited by 1
Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom'proof · cited by 0