Square_Modulo_3
Provedmodulo-arithmeticproofwikisquare-numbers
For any integer x, x^2 mod 3 is 0 or 1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Square_Modulo_3 (x : Int) : x ^ 2 % 3 = 0 \/ x ^ 2 % 3 = 1 := by sorry
Source