lean_workbook_plus_7123

Proved

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

Apply Zsigmondy's theorem to show that there exists a prime $p$ dividing $10^{11} - 1$ and not dividing 9.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7123 (hx: 1 < 10) (h : 11 ≠ 0): ∃ p, p ∣ 10^11 - 1 ∧ ¬ p ∣ 9   :=  by sorry

Source