mem_nthRootsFinset

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

URI: https://scilib.ai/kg/mathlib#IsPrimitiveRoot.mem_nthRootsFinset

← MathLib Explorer

English

If ζ is primitive of order k, then ζ is in nthRootsFinset k (1 in R).

Русский

Если ζ примитивен порядка k, то ζ принадлежит nthRootsFinset k (1 в R).

LaTeX

$$IsPrimitiveRoot(\\zeta, k) \\Rightarrow 0 < k \\Rightarrow \\zeta ∈ nthRootsFinset(k, 1)$$

Lean4

nonrec theorem mem_nthRootsFinset (hζ : IsPrimitiveRoot ζ k) (hk : 0 < k) : ζ ∈ nthRootsFinset k (1 : R) :=
  (mem_nthRootsFinset hk (1 : R)).2 hζ.pow_eq_one

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru