lean_workbook_plus_67806

Proved

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

A number $\overline{abcd}$ is divisible by 8 iff $\overline{bcd}$ is divisible by 8.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67806 : ∀ a b c d : ℕ, a * 10 ^ 3 + b * 10 ^ 2 + c * 10 + d ≡ 0 [ZMOD 8] ↔ b * 10 ^ 2 + c * 10 + d ≡ 0 [ZMOD 8]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph