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.