lean_workbook_plus_13078

Proved

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

Prove that for every positive integer $n$ there are positive integers $a$ and $b$ exist with $n | 4a^2 + 9b^2 -1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13078 (n : ℕ) : ∃ a b : ℕ, n ∣ 4*a^2 + 9*b^2 - 1   :=  by sorry

Source