Integer_to_Power_of_p_1_over_2_Modulo_p
Provedmodular-arithmeticnumber-theoryproofwiki
Let a be an integer and p be an odd prime. Then a^((p-1)/2) mod p is 0, 1, or p-1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Integer_to_Power_of_p_1_over_2_Modulo_p (a : ℤ) (p : ℕ) (hp : Nat.Prime p) (hodd : p % 2 = 1) : a ^ ((p - 1) / 2) % (p : ℤ) = 0 ∨ a ^ ((p - 1) / 2) % (p : ℤ) = 1 ∨ a ^ ((p - 1) / 2) % (p : ℤ) = (p : ℤ) - 1 := by sorry
Source