# mathlibdocumentation

group_theory.commuting_probability

# 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.
noncomputable def comm_prob (M : Type u_1) [fintype M] [has_mul M] :

The commuting probability of a finite type with a multiplication operation

Equations
theorem comm_prob_def (M : Type u_1) [fintype M] [has_mul M] :
= (fintype.card {p // p.fst * p.snd = p.snd * p.fst}) / (fintype.card M) ^ 2
theorem comm_prob_pos (M : Type u_1) [fintype M] [has_mul M] [h : nonempty M] :
0 <
theorem comm_prob_le_one (M : Type u_1) [fintype M] [has_mul M] :
1
theorem comm_prob_eq_one_iff {M : Type u_1} [fintype M] [has_mul M] [h : nonempty M] :
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} =
theorem comm_prob_def' (G : Type u_2) [group G] [fintype G] :
theorem subgroup.comm_prob_subgroup_le {G : Type u_2} [group G] [fintype G] (H : subgroup G) :
* (H.index) ^ 2
theorem subgroup.comm_prob_quotient_le {G : Type u_2} [group G] [fintype G] (H : subgroup G) [H.normal] :