# Commuting Probability #

This file introduces the commuting probability of finite groups.

## Main definitions #

• commProb: The commuting probability of a finite type with a multiplication operation.

## Todo #

• Neumann's theorem.
def commProb (M : Type u_1) [Mul M] :

The commuting probability of a finite type with a multiplication operation.

Equations
Instances For
theorem commProb_def (M : Type u_1) [Mul M] :
= (Nat.card { p : M × M // Commute p.1 p.2 }) / () ^ 2
theorem commProb_prod (M : Type u_1) [Mul M] (M' : Type u_2) [Mul M'] :
commProb (M × M') = * commProb M'
theorem commProb_pi {α : Type u_2} (i : αType u_3) [] [(a : α) → Mul (i a)] :
commProb ((a : α) → i a) = a : α, commProb (i a)
theorem commProb_function {α : Type u_2} {β : Type u_3} [] [Mul β] :
commProb (αβ) =
@[simp]
theorem commProb_eq_zero_of_infinite (M : Type u_1) [Mul M] [] :
= 0
theorem commProb_pos (M : Type u_1) [Mul M] [] [h : ] :
0 <
theorem commProb_le_one (M : Type u_1) [Mul M] [] :
1
theorem commProb_eq_one_iff {M : Type u_1} [Mul M] [] [h : ] :
= 1 Commutative fun (x x_1 : M) => x * x_1
theorem commProb_def' (G : Type u_2) [] :
= () / ()
theorem Subgroup.commProb_subgroup_le {G : Type u_2} [] [] (H : ) :
commProb H * H.index ^ 2
theorem Subgroup.commProb_quotient_le {G : Type u_2} [] [] (H : ) [H.Normal] :
commProb (G H) * (Nat.card H)
theorem inv_card_commutator_le_commProb (G : Type u_2) [] [] :
((Nat.card ()))⁻¹
theorem DihedralGroup.commProb_odd {n : } (hn : Odd n) :
= (n + 3) / (4 * n)
@[irreducible]

A list of Dihedral groups whose product will have commuting probability 1 / n.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem DihedralGroup.reciprocalFactors_even {n : } (h0 : n 0) (h2 : Even n) :
theorem DihedralGroup.reciprocalFactors_odd {n : } (h1 : n 1) (h2 : Odd n) :
@[reducible, inline]

A finite product of Dihedral groups.

Equations
Instances For
@[irreducible]

Construction of a group with commuting probability 1 / n.