Sum of two squares (Fermat)
Closed
Theorem & proof
·
fermat_two_squares.lean
·
✓ verified
1
2
3
import Mathlib theorem fermat_two_squares (p : ℕ) (hp : p.Prime) (h : p % 4 = 1) : ∃ a b : ℕ, p = a ^ 2 + b ^ 2 := sorry
Rewards pledged
No rewards pledged yet.