Quadratic residues satisfy $a^{(p-1)/2}\equiv 1 \pmod p$

Proved

AlfutovaUstinov.problem_4_125

by evgeth · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementary-number-theoryfermat-little-theoremnumber-theoryquadratic-residues

This is Problem 4.125 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”.

Theorem. Let $p>2$ be a prime and let $a$ be an integer not divisible by $p$ . Suppose that $a$ is a square modulo $p$ , i.e. there is an integer $x$ with

x^{2}\equiv a \pmod p .

Then

a^{\frac{p-1}{2}} \equiv 1 \pmod p .

This is one half of Euler's criterion for quadratic residues; the book uses it to study which primes divide numbers of the form $x^2+1$ .

Formalization Note The exponent $(p-1)/2$ is natural-number division, which is exact because $p$ is odd. Congruences are Int.ModEq on $\mathbb Z$ .

Preamble

import Mathlib

Formal statement

namespace AlfutovaUstinov

theorem problem_4_125 (p : ℕ) (hp : p.Prime) (hp2 : 2 < p) (a x : ℤ) (ha : ¬ (p : ℤ) ∣ a)
    (hx : x ^ 2 ≡ a [ZMOD p]) : a ^ ((p - 1) / 2) ≡ 1 [ZMOD p] := by sorry

end AlfutovaUstinov

Source

N. B. Alfutova, A. V. Ustinov, «Алгебра и теория чисел. Сборник задач для математических школ» (Algebra and Number Theory: a problem book for mathematical schools), Moscow: MCCME, 2002, Chapter 4 «Арифметика остатков» (Arithmetic of residues), §4 «Теоремы Ферма и Эйлера» (Theorems of Fermat and Euler), Problem 4.125. Problem text and answer as catalogued on problems.ru, problem 60751: https://problems.ru/view_problem_details_new.php?id=60751

View graph

Quadratic residues satisfy a(p−1)/2≡1(modp)a^{(p-1)/2}\equiv 1 \pmod pa(p−1)/2≡1(modp)

Quadratic residues satisfy $a^{(p-1)/2}\equiv 1 \pmod p$