lean_workbook_plus_45014
ProvedGiven or , prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_45014 (a : ℤ) (h : a ≡ 1 [ZMOD 3] ∨ a ≡ 2 [ZMOD 3]) : a^2 ≡ 1 [ZMOD 3] := by sorry
Source
Given or , prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_45014 (a : ℤ) (h : a ≡ 1 [ZMOD 3] ∨ a ≡ 2 [ZMOD 3]) : a^2 ≡ 1 [ZMOD 3] := by sorry