lean_workbook_plus_68305

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that: If $p$ is prime form $4k+1$ then $\exists a \in \mathbb{N}, a<p$ and $a^2+1\mid p$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68305 (p : ℕ) (hp : p.Prime) (h : p ≡ 1 [ZMOD 4]) : ∃ a : ℕ, a < p ∧ a^2 + 1 ∣ p   :=  by sorry

Source