# mathlib3documentation

group_theory.commuting_probability

# Commuting Probability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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) [has_mul M] :

The commuting probability of a finite type with a multiplication operation

Equations
theorem comm_prob_def (M : Type u_1) [has_mul M] :
= (nat.card {p // p.fst * p.snd = p.snd * p.fst}) / (nat.card M) ^ 2
theorem comm_prob_pos (M : Type u_1) [has_mul M] [finite M] [h : nonempty M] :
0 <
theorem comm_prob_le_one (M : Type u_1) [has_mul M] [finite M] :
1
theorem comm_prob_eq_one_iff {M : Type u_1} [has_mul M] [finite M] [h : nonempty M] :
theorem card_comm_eq_card_conj_classes_mul_card (G : Type u_2) [group G] [finite G] :
nat.card {p // p.fst * p.snd = p.snd * p.fst} =
theorem comm_prob_def' (G : Type u_2) [group G] [finite G] :
theorem subgroup.comm_prob_subgroup_le {G : Type u_2} [group G] [finite G] (H : subgroup G) :
* (H.index) ^ 2
theorem subgroup.comm_prob_quotient_le {G : Type u_2} [group G] [finite G] (H : subgroup G) [H.normal] :