lean_workbook_plus_4234
Proved(a+b)^2-ab=a^2+b^2+ab\equiv 0\pmod{5}\Rightarrow 4a^2+4b^2+4ab\equiv 0\pmod{5}\Rightarrow (2a+b)^2+3b^2\equiv 0\pmod{5}$ .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_4234 (a b : ℤ) : (a + b) ^ 2 - a * b ≡ 0 [ZMOD 5] ↔ (2 * a + b) ^ 2 + 3 * b ^ 2 ≡ 0 [ZMOD 5] := by sorry
Source