lean_workbook_plus_72783

Proved

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

For a 3 digit number to be divisible by $6$ , the 3 digit number should be divisible by both $3$ and $2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72783 (a b c : ℕ) (h₁ : 1 ≤ a ∧ a ≤ 9) (h₂ : 0 ≤ b ∧ b ≤ 9) (h₃ : 0 ≤ c ∧ c ≤ 9) : a * 100 + b * 10 + c ≡ 0 [ZMOD 6] ↔ a * 100 + b * 10 + c ≡ 0 [ZMOD 3] ∧ a * 100 + b * 10 + c ≡ 0 [ZMOD 2]   :=  by sorry

Source

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

View graph