commProb — Mathlib

English

The commuting probability of a finite type M with a multiplication operation is the proportion of commuting pairs in M × M.

Русский

Вероятность того, что два случайно выбранных элемента группы коммутируют, равна доле пары (a,b) ∈ M×M с ab = ba.

LaTeX

$$commProb(M) = |{ p ∈ M × M : Commute p.1 p.2 }| / |M|^2$$

Lean4

/-- The commuting probability of a finite type with a multiplication operation. -/
def commProb : ℚ :=
  Nat.card { p : M × M // Commute p.1 p.2 } / (Nat.card M : ℚ) ^ 2

Похожие утверждения