English
α is defined as the pair (0,1) in X_q, representing √3.
Русский
α определяется как пара (0,1) в X_q, представляющая √3.
LaTeX
$$$ \alpha : X q = (0,1) $$$
Lean4
/-- The final evaluation needed to establish the Lucas-Lehmer necessity. -/
theorem ω_pow_trace [Fact q.Prime] (odd : Odd q) (leg3 : legendreSym q 3 = -1) (leg2 : legendreSym q 2 = 1)
(hq4 : 4 ∣ q + 1) : (ω : X q) ^ ((q + 1) / 4) + ωb ^ ((q + 1) / 4) = 0 :=
by
have : (ω : X q) ^ ((q + 1) / 2) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4) :=
by
rw [pow_ω odd leg3 leg2]
ring
have div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4 := by rcases hq4 with ⟨k, hk⟩; omega
rw [div4, pow_add, mul_assoc, ← mul_pow, ω_mul_ωb, one_pow, mul_one] at this
rw [this]
ring
