ne_one

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

English

If 1 < k then ζ ≠ 1.

Русский

Если 1 < k, то ζ не равно 1.

LaTeX

$$$1 < k \Rightarrow \zeta \neq 1$$$

Lean4

theorem ne_one (h : IsPrimitiveRoot ζ k) (hk : 1 < k) : ζ ≠ 1 :=
  h.pow_ne_one_of_pos_of_lt one_ne_zero hk ∘ (pow_one ζ).trans

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

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

Разделы

Аффилиация

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