lean_workbook_plus_47140

Proved

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

With $n$ is odd, then $10 ^ n + (- 1) ^ {n + 1} = 100...01$ ( $n-1$ of digit $9$ ). Thus $11|10 ^ n + (- 1) ^ {n + 1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47140 (n : ℕ) (hn : Odd n) : 11 ∣ (10 ^ n + (- 1) ^ (n + 1))   :=  by sorry

Source