Theorems · Theorem · group theory

Equiv.Perm.sign_of_cycleType_eq_replicate

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ},
  0 < n →
    σ.cycleType = Multiset.replicate σ.cycleType.card n →
      Equiv.Perm.sign σ = if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

Defined in: Mathlib.GroupTheory.Perm.Cycle.Type
Cited by: 1 results in Mathlib
Foundations: Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites32

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
Fintypestatement and proof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
MonoidHomstatement · cited by 3,629
Unitsstatement and proof · cited by 2,804
Multisetstatement and proof · cited by 2,627
Fintype.cardstatement and proof · cited by 1,386
Equiv.Permstatement and proof · cited by 1,375
neg_negproof · cited by 960
Multiset.mapproof · cited by 876
Multiset.prodproof · cited by 528

Cited by1

Results whose statement or proof uses this declaration.

Equiv.Perm.sign_of_pow_two_eq_oneproof · cited by 1