commProb_def' — Mathlib

English

For a finite group G, the commuting probability equals the number of conjugacy classes divided by the order of G: commProb(G) = |ConjClasses(G)| / |G|.

Русский

Для конечной группы G commuting probability равна числу сопряжённых классов делённому на порядок G: commProb(G) = |ConjClasses(G)| / |G|.

LaTeX

$$commProb(G) = \frac{\#\mathrm{ConjClasses}(G)}{\#G}$$

Lean4

theorem commProb_def' : commProb G = Nat.card (ConjClasses G) / Nat.card G :=
  by
  rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
  by_cases h : (Nat.card G : ℚ) = 0
  · rw [h, zero_mul, div_zero, div_zero]
  · exact mul_div_mul_right _ _ h

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