card_zmod — Mathlib

English

For all n ∈ ℕ, the cardinality of ZMod n equals n (with the case n = 0 giving an infinite type).

Русский

Для всех n ∈ ℕ кардинальность ZMod n равна n (случай n = 0 даёт бесконечный тип).

LaTeX

$$$$ \operatorname{card}(\mathbb{Z}/n\mathbb{Z}) = n \quad (n > 0), \text{ and is infinite when } n=0. $$$$

Lean4

@[simp]
theorem card_zmod (n : ℕ) : Nat.card (ZMod n) = n := by
  cases n
  · exact @Nat.card_eq_zero_of_infinite _ Int.infinite
  · rw [Nat.card_eq_fintype_card, ZMod.card]

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