equiv.perm : card of centralizers and of conjugacy classes

Stream: maths

[Antoine Chambert-Loir]

These two theorems are now known to Lean!

/-- Cardinality of a centralizer in `equiv.perm α` of a given `cycle_type` -/
theorem equiv.perm.conj_stabilizer_card (g : equiv.perm α) (l : list ℕ)
  (hl : g.cycle_type = l) :
  fintype.card (mul_action.stabilizer (conj_act (equiv.perm α)) g) =
   (fintype.card α - l.sum).factorial * (l.prod *
    (list.map (λ (n : ℕ), (list.count n l).factorial) l.dedup).prod) :=  sorry

/-- Cardinality of a conjugacy class in `equiv.perm α` of a given `cycle_type` -/
theorem equiv.perm.conj_class_card (g : equiv.perm α) (l : list ℕ)
  (hl : g.cycle_type = l) :
  fintype.card ({ h : equiv.perm α | is_conj g h}) =
  (fintype.card α).factorial / ((fintype.card α - l.sum).factorial * (l.prod *
    (list.map (λ (n : ℕ), (list.count n l).factorial) l.dedup).prod)) :=  sorry

The proof is ~ 2000 lines long, there will be a PR soon…