lean_workbook_plus_4816

Proved

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

Prove that if $a$ and $b$ are integers that leave the same remainder when divided by 8, then $a^2$ and $b^2$ also leave the same remainder when divided by 8.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4816 {a b : ℤ} (h : a % 8 = b % 8) : a^2 % 8 = b^2 % 8   :=  by sorry

Source

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

View graph