lean_workbook_plus_53377
ProvedProve that if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53377 : ∀ n : ℤ, n ≡ 1 [ZMOD 3] → n ^ 2 + 2 ≡ 0 [ZMOD 3] := by sorry
Source
Prove that if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_53377 : ∀ n : ℤ, n ≡ 1 [ZMOD 3] → n ^ 2 + 2 ≡ 0 [ZMOD 3] := by sorry