English
A variant statement: there are exactly ⌊N/n⌋ multiples of n in the interval [1, N].
Русский
Альтернативное утверждение: в интервале [1, N] ровно ⌊N/n⌋ кратностей n.
LaTeX
$$$ \#\{ k \in [1, N] \mid n \mid k \} = \left\lfloor\dfrac{N}{n}\right\rfloor $$$
Lean4
/-- There are exactly `⌊N/n⌋` positive multiples of `n` that are `≤ N`.
See `Nat.card_multiples` for a "shifted-by-one" version. -/
theorem card_multiples' (N n : ℕ) : #({k ∈ range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n := by
induction N with
| zero => simp [Finset.filter_false_of_mem]
| succ N ih =>
rw [Finset.range_add_one, Finset.filter_insert]
by_cases h : n ∣ N.succ
· simp [h, succ_div_of_dvd, ih]
· simp [h, succ_div_of_not_dvd, ih]
