lean_workbook_plus_75144

Proved

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

The least 3-digit integer that is divisible by 7 is $105=7\cdot15$ . The greatest is $994=7\cdot 142$ . The 3-digit integers that are divisible by $7$ are the $15^\text{th}$ multiple to the $142^\text{nd}$ multiple inclusive. This is $142-15+1=128$ 3-digit numbers that are divisible by $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75144  (n : ℕ)
  (h₀ : 7 * 15 ≤ n)
  (h₁ : n ≤ 7 * 142) :
  Finset.card (Finset.filter (λ x => 7∣x) (Finset.Icc 100 999)) = 128   :=  by sorry

Source

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

View graph