eq_neg_one_of_two_right

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

← MathLib Explorer

English

In a domain with NoZeroDivisors, a primitive root of order 2 is equal to -1.

Русский

В домене без нулевых делителей примитивный корень порядка 2 равен -1.

LaTeX

$$[NoZeroDivisors R] IsPrimitiveRoot(ζ, 2) ⇒ ζ = -1$$

Lean4

theorem eq_neg_one_of_two_right [NoZeroDivisors R] {ζ : R} (h : IsPrimitiveRoot ζ 2) : ζ = -1 :=
  (sq_eq_one_iff.mp h.pow_eq_one).resolve_left <| ne_one h one_lt_two

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

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

Разделы

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

Аффилиация

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