mathlib documentation

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

comm_prob M = ↑(fintype.card {p // p.fst * p.snd = p.snd * p.fst}) / ↑(fintype.card M) ^ 2

theorem comm_prob_def (M : Type u_1) [fintype M] [has_mul M] :

comm_prob 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 < comm_prob M

theorem comm_prob_le_one (M : Type u_1) [fintype M] [has_mul M] :

comm_prob M ≤ 1

theorem comm_prob_eq_one_iff {M : Type u_1} [fintype M] [has_mul M] [h : nonempty M] :

comm_prob M = 1 ↔ commutative has_mul.mul

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} = fintype.card (conj_classes G) * fintype.card G

theorem comm_prob_def' (G : Type u_2) [group G] [fintype G] :

comm_prob G = ↑(fintype.card (conj_classes G)) / ↑(fintype.card G)

theorem subgroup.comm_prob_subgroup_le {G : Type u_2} [group G] [fintype G] (H : subgroup G) :

comm_prob ↥H ≤ comm_prob G * ↑(H.index) ^ 2

theorem subgroup.comm_prob_quotient_le {G : Type u_2} [group G] [fintype G] (H : subgroup G) [H.normal] :

comm_prob (G ⧸ H) ≤ comm_prob G * ↑(fintype.card ↥H)

theorem inv_card_commutator_le_comm_prob (G : Type u_2) [group G] [fintype G] :

(↑(fintype.card ↥(commutator G)))⁻¹ ≤ comm_prob G