primitiveRoots — Mathlib

English

The set primitiveRoots(k,R) consists of primitive k-th roots of unity in the domain R.

Русский

Множество primitiveRoots(k,R) состоит из примитивных k-ых корней единицы в области R.

LaTeX

$$$\mathrm{primitiveRoots}(k,R) = \{ \zeta \in (\mathrm{nthRoots}(k,1)) : \mathrm{IsPrimitiveRoot}(\zeta,k) \}$$$

Lean4

/-- `primitiveRoots k R` is the finset of primitive `k`-th roots of unity
in the integral domain `R`. -/
def primitiveRoots (k : ℕ) (R : Type*) [CommRing R] [IsDomain R] : Finset R :=
  {ζ ∈ (nthRoots k (1 : R)).toFinset | IsPrimitiveRoot ζ k}

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