lean_workbook_plus_64100
ProvedProof:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64100 {n:ℤ} : n % 3 = 0 ∨ n % 3 = 1 ∨ n % 3 = 2 → n ^ 2 % 3 = 0 ∨ n ^ 2 % 3 = 1 := by sorrySource
Proof:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_64100 {n:ℤ} : n % 3 = 0 ∨ n % 3 = 1 ∨ n % 3 = 2 → n ^ 2 % 3 = 0 ∨ n ^ 2 % 3 = 1 := by sorry