English
For a prime p and a not divisible by p, a^{p/2} ≡ (-1)^{N} (mod p), where N counts the x in a certain range with p/2 < (a x) mod p.
Русский
Для простого p и a, не делящегося на p, выполняется: a^{p/2} ≡ (-1)^{N} (mod p), где N — число x из заданного диапазона, для которых p/2 < (a x) mod p.
LaTeX
$$$a^{p/2} \equiv (-1)^{\#\{ x \in Ico(1, p/2).succ \mid p/2 < (a \cdot x.cast) \bmod p \}} \pmod p$$$
Lean4
theorem gauss_lemma_aux (p : ℕ) [hp : Fact p.Prime] {a : ℤ} (hap : (a : ZMod p) ≠ 0) :
(a ^ (p / 2) : ZMod p) = ((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}) :) :=
(mul_left_inj'
(show ((p / 2)! : ZMod p) ≠ 0
by
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]
exact Nat.div_lt_self hp.1.pos (by decide))).1 <|
by simpa using gauss_lemma_aux₁ p hap
