card_commute_odd — Mathlib

English

If n is odd, the number of commuting pairs in DihedralGroup n is n(n+3).

Русский

Если n нечетно, количество коммутирующих пар в DihedralGroup n равно n(n+3).

LaTeX

$$\#\{ p : DihedralGroup(n) × DihedralGroup(n) \mid Commute(p.1,p.2) \} = n(n+3)$$

Lean4

/-- If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs of commuting elements. -/
theorem card_commute_odd (hn : Odd n) :
    Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } = n * (n + 3) :=
  by
  have hn' : NeZero n := ⟨hn.pos.ne'⟩
  simp_rw [Nat.card_congr (oddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]
  ring

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