lean_workbook_plus_52521
ProvedProve that if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52521 {n : ℤ} (h : n ≡ 1 [ZMOD 4] ∨ n ≡ 3 [ZMOD 4]) : n ^ 2 ≡ 1 [ZMOD 4] := by sorrySource
Prove that if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_52521 {n : ℤ} (h : n ≡ 1 [ZMOD 4] ∨ n ≡ 3 [ZMOD 4]) : n ^ 2 ≡ 1 [ZMOD 4] := by sorry