iff_orderOf

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

English

For any ζ, IsPrimitiveRoot ζ k holds iff orderOf ζ = k.

Русский

Для любого ζ IsPrimitiveRoot(ζ,k) эквивалентно orderOf ζ = k.

LaTeX

$$$$\mathrm{IsPrimitiveRoot}(\zeta,k) \iff \mathrm{orderOf}(\zeta) = k.$$$$

Lean4

protected theorem iff_orderOf : IsPrimitiveRoot ζ k ↔ orderOf ζ = k :=
  not_iff_not.mp IsPrimitiveRoot.not_iff

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

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

Разделы

Аффилиация

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