Prove2Me

lean_workbook_plus_58004

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let's look at the squares of non-zero elements. If x2=ax^2=a , then (−x)2=a(-x)^2=a , and x≠−xx\ne -x for all non-zero xx . This means that the only way we can have n−12\frac {n-1}2 non-zero squares is if x2=y2x^2=y^2 implies x=yx=y or x=−yx=-y .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58004  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : ∀ x : ZMod n, x ≠ 0 → ∃! y, y^2 = x^2) :
  ∀ x : ZMod n, x ≠ 0 → ∀ y : ZMod n, y ≠ 0 → x^2 = y^2 → x = y ∨ x = -y   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph