mathlib documentation

group_theory.commuting_probability

Commuting Probability #

This file introduces the commuting probability of finite groups.

Main definitions #

Todo #

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] :
comm_prob 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] :
theorem comm_prob_le_one (M : Type u_1) [has_mul M] [finite M] :