lean_workbook_plus_66087

Proved

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

Using Fermat's Little Theorem (FLT), show that for $a\not\equiv 0\pmod{3}$ , $a^2\equiv 1\pmod{3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66087 (a : ℤ) (ha : ¬ a ≡ 0 [ZMOD 3]) : a ^ 2 ≡ 1 [ZMOD 3]   :=  by sorry

Source