neg_one — Mathlib

English

For suitable p, the element -1 is a primitive 2nd root of unity.

Русский

При некоторых p элемент -1 является примитивным корнем корня единицы второй степени.

LaTeX

$$IsPrimitiveRoot(-1, 2)$$

Lean4

theorem neg_one (p : ℕ) [Nontrivial R] [h : CharP R p] (hp : p ≠ 2) : IsPrimitiveRoot (-1 : R) 2 :=
  by
  convert IsPrimitiveRoot.orderOf (-1 : R)
  rw [orderOf_neg_one, if_neg <| by rwa [ringChar.eq_iff.mpr h]]

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