mathlib documentation


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 #

Todo #

noncomputable def comm_prob (M : Type u_1) [has_mul M] :

The commuting probability of a finite type with a multiplication operation

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] :