card_eq_totient_of_hasEnoughRootsOfUnity

English

There are exactly φ(n) Dirichlet characters modulo n (over rings with enough roots of unity).

Русский

Существует ровно φ(n) символов Дирихле модуля n (в окружении, где достаточно корней корней единства).

LaTeX

$$$\\operatorname{card}(\\text{DirichletCharacter}(R,n)) = n^{\\;\\mathrm{totient}}.$$$

Lean4

/-- There are `n.totient` Dirichlet characters mod `n` with values in a ring that has enough
roots of unity. -/
theorem card_eq_totient_of_hasEnoughRootsOfUnity : Nat.card (DirichletCharacter R n) = n.totient :=
  by
  rw [← ZMod.card_units_eq_totient n, ← Nat.card_eq_fintype_card]
  exact Nat.card_congr (mulEquiv_units R n).some.toEquiv

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