Counting multiples of two, three or five
ProvedWorkbookSyntax.plus_43171lean-workbookrepaired-notationsource-checked
Exactly1,469 integers in are divisible by at least one of2,3 or5.
Notation repair: Replaced the obsolete finite-sum binder “in” with the current “∈” notation. The ranges, summands, hypotheses and conclusion are unchanged.
Source: Lean-Workbook record lean_workbook_plus_43171 (Apache-2.0). Original declaration.
Preamble
import Mathlib open Nat
Formal statement
theorem WorkbookSyntax.plus_43171 : ∑ k ∈ Finset.filter (λ x => 2∣x ∨ 3∣x ∨ 5∣x) (Finset.Icc 1 2004), 1 = 1469 := by sorry
Source