card_nthRootsFinset — Mathlib

English

The set of nth roots of one is the union, over all divisors i of n, of the sets primitiveRoots i R.

Русский

Множество n-й корней единицы равно объединению по i|n множеств primitiveRoots i R.

LaTeX

$$$\operatorname{nthRootsFinset}(n,1) = \bigcup_{i \mid n} \operatorname{primitiveRoots}(i,R)$$$

Lean4

theorem card_nthRootsFinset {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : #(nthRootsFinset n (1 : R)) = n := by
  classical rw [nthRootsFinset, ← Multiset.toFinset_eq (nthRoots_one_nodup h), card_mk, h.card_nthRoots_one]

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