Documentation

Mathlib.GroupTheory.CommutingProbability

Commuting Probability #

This file introduces the commuting probability of finite groups.

Main definitions #

Todo #

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] :
    commProb M = (Nat.card { p : M × M // Commute p.1 p.2 }) / (Nat.card M) ^ 2
    theorem commProb_prod (M : Type u_1) [Mul M] (M' : Type u_2) [Mul M'] :
    theorem commProb_pi {α : Type u_3} (i : αType u_2) [Fintype α] [(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} [Fintype α] [Mul β] :
    commProb (αβ) = commProb β ^ Fintype.card α
    @[simp]
    theorem commProb_eq_zero_of_infinite (M : Type u_1) [Mul M] [Infinite M] :
    theorem commProb_pos (M : Type u_1) [Mul M] [Finite M] [h : Nonempty M] :
    theorem commProb_le_one (M : Type u_1) [Mul M] [Finite M] :
    theorem commProb_eq_one_iff {M : Type u_1} [Mul M] [Finite M] [h : Nonempty M] :
    commProb M = 1 Commutative fun (x x_1 : M) => x * x_1
    theorem commProb_def' (G : Type u_2) [Group G] :
    theorem DihedralGroup.commProb_odd {n : } (hn : Odd n) :
    commProb (DihedralGroup 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
      @[inline, reducible]

      A finite product of Dihedral groups.

      Equations
      Instances For

        Construction of a group with commuting probability 1 / n.