mem_primitiveRoots — Mathlib

English

If k>0, then an element ζ lies in primitiveRoots(k,R) if and only if ζ is a primitive k-th root of unity.

Русский

Если k>0, то элемент ζ принадлежит primitiveRoots(k,R) тогда и только тогда, когда ζ является примитивным k-ым корнем единицы.

LaTeX

$$$\zeta \in \mathrm{primitiveRoots}(k,R) \iff \mathrm{IsPrimitiveRoot}(\zeta,k)$$$

Lean4

@[simp]
theorem mem_primitiveRoots {ζ : R} (h0 : 0 < k) : ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k := by
  classical
  rw [primitiveRoots, mem_filter, Multiset.mem_toFinset, mem_nthRoots h0, and_iff_right_iff_imp]
  exact IsPrimitiveRoot.pow_eq_one

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