nthRoots_one_nodup — Mathlib

English

The finset of nth roots of unity has cardinality n when a primitive root exists.

Русский

Число элементов конечного множества nthRootsFinset равно n, если существует примитивный корень.

LaTeX

$$$\#(nthRootsFinset n 1) = n$$$

Lean4

/-- The multiset `nthRoots ↑n (1 : R)` has no repeated elements
if there is a primitive root of unity in `R`. -/
theorem nthRoots_one_nodup {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRoots n (1 : R)).Nodup :=
  h.nthRoots_nodup one_ne_zero

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