lean_workbook_plus_2406

Proved

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

For prime $p\equiv 1\pmod{7}$ , prove that there exists some positive integer $m$ such that $m^3+m^2-2m-1$ is a multiple of $p$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2406 (p : ℕ) (hp : p.Prime) (hp1 : p ≡ 1 [ZMOD 7]) : ∃ m : ℕ, ((7 : ℤ)∣(m^3 + m^2 - 2*m - 1) % p)   :=  by sorry

Source