card_rootsOfUnity — Mathlib

English

Let n be a positive integer. The set of nth roots of unity in the complex numbers has exactly n elements.

Русский

Пусть n — положительное целое. Множество n-ых корней единицы в комплексных числах содержит ровно n элементов.

LaTeX

$$$\\#\\{ z \\in \\mathbb{C} \\mid z^n = 1 \\} = n$$$

Lean4

theorem card_rootsOfUnity (n : ℕ) [NeZero n] : Fintype.card (rootsOfUnity n ℂ) = n :=
  (isPrimitiveRoot_exp n NeZero.out).card_rootsOfUnity

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