English
If n = x^2 + y^2 with gcd(x,y)=1, then -1 is a square modulo n, i.e., there exists t with t^2 ≡ -1 (mod n).
Русский
Если n выражимо как сумма квадратов x^2 + y^2 и gcd(x,y)=1, то -1 является квадратом в Z/nZ, то есть найдётся t such that t^2 ≡ -1 (mod n).
LaTeX
$$$\\text{If } n=x^2+y^2 \\text{ and } \\gcd(x,y)=1,\\quad -1 \\text{ is a square modulo } n,$ i.e. $\\exists t:\\; t^2 \\equiv -1 \\pmod n$.$$
Lean4
/-- If the integer `n` is a sum of two squares of coprime integers,
then `-1` is a square modulo `n`. -/
theorem isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime {n x y : ℤ} (h : n = x ^ 2 + y ^ 2) (hc : IsCoprime x y) :
IsSquare (-1 : ZMod n.natAbs) :=
by
obtain ⟨u, v, huv⟩ : IsCoprime x n :=
by
have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
rw [show y ^ 2 = n + -1 * x ^ 2 by cutsat] at hc2
exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right
have H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v) := by
linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv
refine ⟨u * y, ?_⟩
conv_rhs => tactic => norm_cast
rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]
exact (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)
