card — Mathlib

English

For NeZero n, the cardinality of DihedralGroup n is 2n.

Русский

Для любого положительного n кардинальность DihedralGroup n равна 2n.

LaTeX

$$[NeZero n] \Rightarrow Fintype.card(DihedralGroup(n)) = 2 \cdot n$$

Lean4

/-- If `0 < n`, then `DihedralGroup n` has `2n` elements.
-/
theorem card [NeZero n] : Fintype.card (DihedralGroup n) = 2 * n := by
  rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]

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