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