commProb_def — Mathlib

English

The commuting probability of a finite type M can be expressed as card of commuting pairs divided by the square of the size of M, interpreted in rationals.

Русский

Вероятность того, что два элемента коммутируют, равна количеству пар, деленному на квадрат размера множества, в рациональном числе.

LaTeX

$$commProb(M) = card{ p ∈ M × M : Commute p.fst p.snd } / (card M)^2$$

Lean4

theorem commProb_def : commProb M = Nat.card { p : M × M // Commute p.1 p.2 } / (Nat.card M : ℚ) ^ 2 :=
  rfl

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