primitiveRoots_one — Mathlib

English

Over a domain, the set of primitive roots of order 1 is {1}.

Русский

В домене множество примитивных корней порядка 1 равно {1}.

LaTeX

$$primitiveRoots(1, R) = {1}$$

Lean4

@[simp]
theorem primitiveRoots_one : primitiveRoots 1 R = {(1 : R)} :=
  by
  refine Finset.eq_singleton_iff_unique_mem.2 ⟨?_, fun x hx ↦ ?_⟩
  · simp only [IsPrimitiveRoot.one_right_iff, mem_primitiveRoots zero_lt_one]
  · rwa [mem_primitiveRoots zero_lt_one, IsPrimitiveRoot.one_right_iff] at hx

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