lean_workbook_plus_66934

Proved

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

Given the identity $4(x^2-xy+y^2)=(2x-y)^2+3y^2$ , if $n=a^2+3b^2 \equiv 0( \text{mod } 4)$ , prove that $a \equiv b(\text{mod }2)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66934 (a b : ℤ) (h : a^2 + 3 * b^2 ≡ 0 [ZMOD 4]) : a ≡ b [ZMOD 2]   :=  by sorry

Source