English
Exactly ⌊n/p⌋ natural numbers between 1 and n are multiples of p; i.e., the count of k ∈ {1,...,n} with p ∣ k is ⌊n/p⌋.
Русский
Точно ⌊n/p⌋ чисел от 1 до n кратны p; то есть число k ∈ {1,...,n} с p|k равно ⌊n/p⌋.
LaTeX
$$$ \#\{ k \in \{1,\dots, n\} \mid p \mid k \} = \left\lfloor\dfrac{n}{p}\right\rfloor $$$
Lean4
/-- Exactly `n / p` naturals in `[1, n]` are multiples of `p`.
See `Nat.card_multiples'` for an alternative spelling of the statement. -/
theorem card_multiples (n p : ℕ) : #({e ∈ range n | p ∣ e + 1}) = n / p := by
induction n with
| zero => simp
| succ n hn =>
simp [Nat.succ_div, add_ite, add_zero, Finset.range_add_one, filter_insert, apply_ite card, card_insert_of_notMem,
hn]
