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) [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] :
theorem comm_prob_pos (M : Type u_1) [fintype M] [has_mul M] [h : nonempty M] :
theorem comm_prob_le_one (M : Type u_1) [fintype M] [has_mul M] :
theorem comm_prob_eq_one_iff {M : Type u_1} [fintype M] [has_mul M] [h : nonempty M] :
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) :
theorem subgroup.comm_prob_quotient_le {G : Type u_2} [group G] [fintype G] (H : subgroup G) [H.normal] :