card_primitiveRoots — Mathlib

English

There are exactly φ(k) primitive k-th roots of unity in the complex numbers; with k = 0 treated suitably.

Русский

В комплексных числах существует ровно φ(k) примитивных k-й корней единицы; случай k = 0 трактуется надлежащим образом.

LaTeX

$$$|\\mathrm{primitiveRoots}(k, \\mathbb{C})| = \\varphi(k)$$$

Lean4

theorem card_primitiveRoots (k : ℕ) : (primitiveRoots k ℂ).card = φ k :=
  by
  by_cases h : k = 0
  · simp [h]
  exact (isPrimitiveRoot_exp k h).card_primitiveRoots

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