lean_workbook_plus_68403

Proved

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

Prove that $11^{10n+k} \equiv 10k+1 \mod 100$ for every integer $k$ and $0 \leq k \leq 9$ and for every positive integer $n$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68403 (k : ℕ) (h₁ : k ≤ 9) (n : ℕ) : (11 ^ (10 * n + k)) % 100 = 10 * k + 1   :=  by sorry

Source