lean_workbook_plus_70637
ProvedActually, for all even it holds that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70637 {z : ℤ} (h : z % 2 = 0) : z ^ 2 ≡ 0 [ZMOD 4] := by sorrySource
Actually, for all even it holds that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_70637 {z : ℤ} (h : z % 2 = 0) : z ^ 2 ≡ 0 [ZMOD 4] := by sorry