lean_workbook_plus_27618

Proved

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

Given $x = 4k + n$ , where $n, k \in \mathbb{Z}$ , show that $x^2 \equiv n^2 \pmod{8}$ if $x \equiv n \pmod{4}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27618 (x n k : ℤ) (h₁ : x ≡ n [ZMOD 4]) : x ^ 2 ≡ n ^ 2 [ZMOD 8]   :=  by sorry

Source