Commuting Probability #
This file introduces the commuting probability of finite groups.
Main definitions #
comm_prob
: The commuting probability of a finite type with a multiplication operation.
Todo #
- Neumann's theorem.
theorem
card_comm_eq_card_conj_classes_mul_card
(G : Type u_2)
[group G]
[fintype G]
[h : fintype (conj_classes G)] :
fintype.card {p // p.fst * p.snd = p.snd * p.fst} = fintype.card (conj_classes G) * fintype.card G
theorem
comm_prob_def'
(G : Type u_2)
[group G]
[fintype G] :
comm_prob G = ↑(fintype.card (conj_classes G)) / ↑(fintype.card G)
theorem
inv_card_commutator_le_comm_prob
(G : Type u_2)
[group G]
[fintype G] :
(↑(fintype.card ↥(commutator G)))⁻¹ ≤ comm_prob G