one_add_α_pow_q_succ

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.X.one_add_α_pow_q_succ

← MathLib Explorer

English

ω · ω_b = 1 in X_q.

Русский

ω · ω_b = 1 в X_q.

LaTeX

$$$ (\omega : X q) \cdot ω_b = 1 $$$

Lean4

/-- If `3` is not a square then `(1 + α) ^ (q + 1) = -2`. -/
theorem one_add_α_pow_q_succ [Fact q.Prime] (odd : Odd q) (leg3 : legendreSym q 3 = -1) :
    (1 + α : X q) ^ (q + 1) = -2 :=
  by
  rw [pow_succ, one_add_α_pow_q odd leg3, mul_comm, ← _root_.sq_sub_sq, α_sq]
  norm_num

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

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

Разделы

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

Аффилиация

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