lean_workbook_plus_34668

Proved

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

We have $p|(q-1)(q^2+q+1)$ and $p$ is a prime so $p|(q-1)$ or $p|(q^2+q+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34668 (p q : ℕ) (hp : p.Prime) : p ∣ (q - 1) * (q ^ 2 + q + 1) → p ∣ q - 1 ∨ p ∣ q ^ 2 + q + 1   :=  by sorry

Source