lean_workbook_plus_28783

Proved

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

Prove that all positive integers are factors of some $10^k(10^m - 1)/9$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28783 (n : ℕ) : ∃ (k : ℕ), ∃ (m : ℕ), n ∣ (10^k * (10^m - 1)) / 9   :=  by sorry

Source