Prove2Me

lean_workbook_plus_6574

Proved

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

∃a,b≤p−12/1+a(p−1)≡1+b(p−1)(modq)\exists a,b\le \frac{p-1}{2} / 1+a(p-1)\equiv 1+b(p-1)\pmod{q}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6574 (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p < q) :
    ∃ a b, a ≤ (p-1)/2 ∧ b ≤ (p-1)/2 ∧ 1 + a * (p-1) ≡ 1 + b * (p-1) [ZMOD q]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph