euler_criterion — Mathlib

English

Let p be prime and a ∈ Z/pZ nonzero. Then a is a square modulo p if and only if a^(p/2) = 1 in Z/pZ.

Русский

Пусть p — простое, и a ∈ Z/pZ непусто. Тогда a является квадратичным остатком по модулю p тогда и только тогда, когда a^(p/2) = 1 в Z/pZ.

LaTeX

$$$\forall a \in Z/pZ,\ a \neq 0:\ IsSquare(a) \iff a^{p/2} = 1$$$

Lean4

/-- Euler's Criterion: a nonzero `a : ZMod p` is a square if and only if `x ^ (p / 2) = 1`. -/
theorem euler_criterion {a : ZMod p} (ha : a ≠ 0) : IsSquare (a : ZMod p) ↔ a ^ (p / 2) = 1 :=
  by
  apply (iff_congr _ (by simp [Units.ext_iff])).mp (euler_criterion_units p (Units.mk0 a ha))
  simp only [Units.ext_iff, sq, Units.val_mk0, Units.val_mul]
  constructor
  · rintro ⟨y, hy⟩; exact ⟨y, hy.symm⟩
  · rintro ⟨y, rfl⟩
    have hy : y ≠ 0 := by
      rintro rfl
      simp [mul_zero, ne_eq] at ha
    refine ⟨Units.mk0 y hy, ?_⟩; simp

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