lean_workbook_plus_45884

Proved

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

If $a,b$ are both odd then $a^2+b^2+c^2 \equiv 2,3 \pmod {4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45884 {a b c : ℤ} (ha : Odd a) (hb : Odd b) : Odd c → a^2 + b^2 + c^2 ≡ 2 [ZMOD 4] ∨ a^2 + b^2 + c^2 ≡ 3 [ZMOD 4]   :=  by sorry

Source

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

View graph