# mathlibdocumentation

order.filter.modeq

# 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.

theorem nat.frequently_mod_eq {d n : } (h : d < n) :
∃ᶠ (m : ) in filter.at_top, m % n = d
theorem nat.frequently_even  :
∃ᶠ (m : ) in filter.at_top, even m
theorem nat.frequently_odd  :
∃ᶠ (m : ) in filter.at_top, odd m