lean_workbook_plus_77094

Disproved

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

If $n\le k$ are positive integers, then $2^n\pmod{10^k}$ is always divisible by $2^k$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77094 : ∀ n k : ℕ, n ≤ k → 2 ^ k ∣ 2 ^ n % 10 ^ k   :=  by sorry

Source