Prove2Me

lean_workbook_plus_76406

Proved

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

x10=1(mod7)⇔x10×2−3×(7−1)=x2=1(mod7) x^{10}=1(mod 7) \Leftrightarrow x^{10 \times 2- 3 \times (7-1)}=x^2=1(mod 7)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76406 (x : ℕ) : x^10 ≡ 1 [ZMOD 7] ↔ x^2 ≡ 1 [ZMOD 7]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph