lean_workbook_plus_75210

Proved

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

Every odd number can be written as $2k+1$ form. So every square of a odd number can be written as $(2k+1)^2=4k^2+4k+1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75210 (n : ℤ) (h : n%2 = 1) : ∃ k, n = 2 * k + 1 ∧ n^2 = 4 * k^2 + 4 * k + 1   :=  by sorry

Source