isSquare_neg_one_of_eq_sq_add_sq_of_coprime

English

A natural number n is a sum of two squares iff there exist a,b ∈ ℕ with n = a^2 b and -1 is a square modulo b.

Русский

Число n является суммой двух квадратов тогда и только тогда, когда существует пара натуральных a,b с n = a^2 b и -1 является квадратом по модулю b.

LaTeX

$$$\\exists a,b\\in\\mathbb{N},\\; n=a^2 b \\land \\text{IsSquare}(-1: ZMod\\ b)$$$

Lean4

/-- If the natural number `n` is a sum of two squares of coprime natural numbers, then
`-1` is a square modulo `n`. -/
theorem isSquare_neg_one_of_eq_sq_add_sq_of_coprime {n x y : ℕ} (h : n = x ^ 2 + y ^ 2) (hc : x.Coprime y) :
    IsSquare (-1 : ZMod n) := by
  zify at h
  exact ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime

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