lean_workbook_plus_23610
ProvedProve that if , then is odd
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23610 {k : ℤ} (h : k ^ 2 ≡ 1 [ZMOD 8]) : Odd k := by sorrySource
Prove that if , then is odd
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_23610 {k : ℤ} (h : k ^ 2 ≡ 1 [ZMOD 8]) : Odd k := by sorry