lean_workbook_plus_6334

Proved

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

Given $n = 4(b+1)$ , conclude that $n$ is a perfect square if $b+1$ is a perfect square.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6334 (b : ℕ) (h₁ : ∃ k : ℕ, k^2 = (b + 1)) : ∃ l : ℕ, l^2 = 4 * (b + 1)   :=  by sorry

Source