lean_workbook_plus_32783

Proved

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

Prove that the square of any odd integer is of the form $8n+1$ or $8n+7$ for some integer $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32783 (n : ℤ) (h : n%2 = 1) : ∃ k : ℤ, n ^ 2 = 8*k + 1 ∨ n ^ 2 = 8*k + 7   :=  by sorry

Source