# Documentation

Mathlib.GroupTheory.CommutingProbability

# 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.

Instances For
theorem commProb_def (M : Type u_1) [Mul M] :
= ↑(Nat.card { p // Commute p.fst p.snd }) / ↑() ^ 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_3} (i : αType u_2) [] [(a : α) → Mul (i a)] :
commProb ((a : α) → i a) = Finset.prod Finset.univ fun 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 => x * x_1
theorem commProb_def' (G : Type u_2) [] :
= ↑() / ↑()
theorem Subgroup.commProb_subgroup_le {G : Type u_2} [] [] (H : ) :
commProb { x // x H } * ↑() ^ 2
theorem Subgroup.commProb_quotient_le {G : Type u_2} [] [] (H : ) [] :
commProb (G H) * ↑(Nat.card { x // x H })
theorem inv_card_commutator_le_commProb (G : Type u_2) [] [] :
(↑(Nat.card { x // x }))⁻¹
theorem DihedralGroup.commProb_odd {n : } (hn : Odd n) :
= (n + 3) / (4 * n)

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) :
@[inline, reducible]

A finite product of Dihedral groups.

Instances For

Construction of a group with commuting probability 1 / n.