lean_workbook_plus_42161

Proved

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

Prove that for all $q\in\mathbb{N}$ with $\gcd(q,10)=1$ , there exists $n\in\mathbb{N}$ such that $q|(10^{n}-1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42161 (q : ℕ) (hq : Nat.Coprime q 10) : ∃ n : ℕ, q ∣ (10^n - 1)   :=  by sorry

Source