sq_add_sq — Mathlib

English

Let R be a ring of characteristic p (prime). For any integer x, there exist natural numbers a,b such that ((a : R)^2 + (b : R)^2) = x in R.

Русский

Пусть R — кольцо характеристикм p (простое). Для любого целого x существуют a,b ∈ ℕ такие, что (a^2 + b^2) в R равняется x.

LaTeX

$$$\\exists a,b \\in \\mathbb{N},\\ ((a : R)^2 + (b : R)^2) = x$$$

Lean4

theorem sq_add_sq (R : Type*) [Ring R] [IsDomain R] (p : ℕ) [NeZero p] [CharP R p] (x : ℤ) :
    ∃ a b : ℕ, ((a : R) ^ 2 + (b : R) ^ 2) = x :=
  by
  haveI := char_is_prime_of_pos R p
  obtain ⟨a, b, hab⟩ := ZMod.sq_add_sq p x
  refine ⟨a.val, b.val, ?_⟩
  simpa using congr_arg (ZMod.castHom dvd_rfl R) hab

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