lean_workbook_plus_59411Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)The base case of n=0n=0n=0 is true. Since 11∣10n+(−1)n+111|10^n+(-1)^{n+1}11∣10n+(−1)n+1 , 10n+(−1)n+1=11m10^n+(-1)^{n+1}=11m10n+(−1)n+1=11m for an integer, mmm . 10n+1+(−1)n+2=10(10n+(−1)n+1)−11(−1)n+1=10(11m)−11((−1)n+1)=11(10m+(−1)n)10^{n+1}+(-1)^{n+2}=10(10^n+(-1)^{n+1})-11(-1)^{n+1}=10(11m)-11((-1)^{n+1})=11(10m+(-1)^n)10n+1+(−1)n+2=10(10n+(−1)n+1)−11(−1)n+1=10(11m)−11((−1)n+1)=11(10m+(−1)n) . We are done.Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_59411 (n : ℕ) : 11 ∣ (10^n + (-1 : ℤ)^(n + 1)) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph