card_conjClasses_odd — Mathlib

English

For odd n, the number of conjugacy classes in DihedralGroup n is (n+3)/2.

Русский

Для нечетного n число классов сопряжённости в DihedralGroup n равно (n+3)/2.

LaTeX

$$\#\mathrm{ConjClasses}(\mathrm{DihedralGroup}(n)) = \dfrac{n+3}{2} \quad (n\ \text{ odd})$$

Lean4

theorem card_conjClasses_odd (hn : Odd n) : Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2 := by
  rw [← Nat.mul_div_mul_left _ 2 hn.pos, ← card_commute_odd hn, mul_comm, card_comm_eq_card_conjClasses_mul_card,
    nat_card, Nat.mul_div_left _ (mul_pos two_pos hn.pos)]

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