commProb_odd — Mathlib

English

For odd n, the commuting probability of the dihedral group D_n is (n+3)/(4n).

Русский

Для нечетного n вероятность коммутирования в группе диагетральных равна (n+3)/(4n).

LaTeX

$$commProb(\mathrm{DihedralGroup}(n)) = \frac{n+3}{4n} \, (\text{для нечетного } n)$$

Lean4

theorem commProb_odd {n : ℕ} (hn : Odd n) : commProb (DihedralGroup n) = (n + 3) / (4 * n) :=
  by
  rw [commProb_def', DihedralGroup.card_conjClasses_odd hn, nat_card]
  qify [show 2 ∣ n + 3 by rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]]
  rw [div_div, ← mul_assoc]
  congr
  norm_num

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