lean_workbook_plus_25568

Proved

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

Given $n = a^2 + 5b^2$ where a and b are integers not equal to 0, express $n^4$ in the form $n^4 = a'^2 + 5b'^2$ where a' and b' are integers.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25568 (n a b : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hab : a * b ≠ 0) (h : n = a^2 + 5 * b^2) : ∃ a' b' : ℤ, a'^2 + 5 * b'^2 = n^4   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph