lean_workbook_plus_31440
Provedquadratic residues mod
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31440 : {0, 1, 4, 7} = {n : ℕ | n < 9 ∧ ∃ k : ℕ, k < 9 ∧ n ≡ k ^ 2 [ZMOD 9]} := by sorrySource
quadratic residues mod
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_31440 : {0, 1, 4, 7} = {n : ℕ | n < 9 ∧ ∃ k : ℕ, k < 9 ∧ n ≡ k ^ 2 [ZMOD 9]} := by sorry