existsUnique

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

English

There exists a unique k such that IsPrimitiveRoot ζ k.

Русский

Существует единственный k, для которого IsPrimitiveRoot ζ k.

LaTeX

$$$$\exists! k, IsPrimitiveRoot(\zeta,k).$$$$

Lean4

theorem existsUnique : ∃! k, IsPrimitiveRoot ζ k :=
  ⟨_, .orderOf _, fun _ hl ↦ unique hl (.orderOf _)⟩

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

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

Разделы

Аффилиация

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