one_add_α_pow_q — Mathlib

English

Defining ω_b as the element (2, -1) in X_q.

Русский

Определение ω_b как элемента (2, −1) в X_q.

LaTeX

$$$ \omega_b = (2,-1) \in X_q $$$

Lean4

/-- If `3` is not a square mod `q` then `(1 + α) ^ q = 1 - α` -/
theorem one_add_α_pow_q [Fact q.Prime] (odd : Odd q) (leg3 : legendreSym q 3 = -1) : (1 + α : X q) ^ q = 1 - α :=
  by
  obtain ⟨k, rfl⟩ := odd
  let q := 2 * k + 1
  have : (3 ^ k : ZMod q) = -1 := by simpa [leg3, mul_add_div, eq_comm] using legendreSym.eq_pow (2 * k + 1) 3
  rw [add_pow_expChar, α_pow, show (3 : X q) = (3 : ZMod q) by rw [map_ofNat], ← map_pow, this, map_neg]
  simp [sub_eq_add_neg]

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