Numbers are frequently modeq to fixed numbers #
In this file we prove that m ≡ d [MOD n]
frequently as m → ∞
.
theorem
nat.frequently_modeq
{n : ℕ}
(h : n ≠ 0)
(d : ℕ) :
∃ᶠ (m : ℕ) in filter.at_top, m ≡ d [MOD n]
Infinitely many natural numbers are equal to d
mod n
.