English
Let p be prime. For every unit x in Z/pZ, x is a square if and only if x^(p/2) = 1 in Z/pZ (with the case p=2 being trivial).
Русский
Пусть p — простое. Для каждого элемента x модульной группы (Z/pZ)× x является квадратичным остатком тогда и только тогда, когда x^(p/2) = 1 (в Z/pZ), исключение p=2 тривиально.
LaTeX
$$$\forall x \in (\mathbb{Z}/p\mathbb{Z})^{\times},\ \big(\exists y:(\mathbb{Z}/p\mathbb{Z})^{\times}, y^2 = x\big) \iff x^{p/2} = 1$ (при p=2 тривиально).$$
Lean4
/-- Euler's Criterion: A unit `x` of `ZMod p` is a square if and only if `x ^ (p / 2) = 1`. -/
theorem euler_criterion_units (x : (ZMod p)ˣ) : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ x ^ (p / 2) = 1 :=
by
by_cases hc : p = 2
· subst hc
simp only [eq_iff_true_of_subsingleton, exists_const]
· have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x
have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x :=
by
rw [isSquare_iff_exists_sq x]
simp_rw [eq_comm]
rw [hs]
rwa [card p] at h₀
