lean_workbook_plus_19450
ProvedProve that for any odd number
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19450 {a : ℤ} (h : a%2 = 1) : a ^ 2 ≡ 1 [ZMOD 2] := by sorrySource
Prove that for any odd number
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_19450 {a : ℤ} (h : a%2 = 1) : a ^ 2 ≡ 1 [ZMOD 2] := by sorry