isPrimitiveRoot_of_mem_primitiveRoots

English

If ζ is an element of R that lies in the set primitiveRoots(k,R), then ζ is a primitive k-th root of unity.

Русский

Пусть ζ ∈ R принадлежит множеству primitiveRoots(k,R); тогда ζ является примитивным корнем k-й степени единицы.

LaTeX

$$$\zeta \in \operatorname{primitiveRoots}(k,R) \implies \operatorname{IsPrimitiveRoot}(\zeta,k)$$$

Lean4

theorem isPrimitiveRoot_of_mem_primitiveRoots {ζ : R} (h : ζ ∈ primitiveRoots k R) : IsPrimitiveRoot ζ k :=
  k.eq_zero_or_pos.elim (fun hk ↦ by simp [hk] at h) fun hk ↦ (mem_primitiveRoots hk).1 h

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