lean_workbook_plus_79076
DisprovedProve that if , then is even.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79076 : ∀ x : ℤ, x ^ 2 ≡ 1 [ZMOD 8] → Even ((x ^ 2 - 1) / 8) := by sorry
Source
Prove that if , then is even.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_79076 : ∀ x : ℤ, x ^ 2 ≡ 1 [ZMOD 8] → Even ((x ^ 2 - 1) / 8) := by sorry