two_mul_ω_pow — Mathlib

English

ω_b · ω = 1 in X_q.

Русский

ω_b · ω = 1 в X_q.

LaTeX

$$$ (\omega_b : X q) \cdot (\omega : X q) = 1 $$$

Lean4

/-- If `3` is not a square then `(2 * ω) ^ ((q + 1) / 2) = -2`. -/
theorem two_mul_ω_pow [Fact q.Prime] (odd : Odd q) (leg3 : legendreSym q 3 = -1) : (2 * ω : X q) ^ ((q + 1) / 2) = -2 :=
  by
  rw [← one_add_α_sq, ← pow_mul]
  have : 2 * ((q + 1) / 2) = q + 1 := by
    apply Nat.mul_div_cancel'
    rw [← even_iff_two_dvd]
    exact Odd.add_one odd
  rw [this, one_add_α_pow_q_succ odd leg3]

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