# Numbers are frequently ModEq to fixed numbers #

In this file we prove that `m ≡ d [MOD n]` frequently as `m → ∞`.

source
theorem Nat.frequently_modEq {n : ℕ} (h : n ≠ 0) (d : ℕ) :
∃ᶠ (m : ℕ) in Filter.atTop, m ≡ d [MOD n]

Infinitely many natural numbers are equal to `d` mod `n`.

source
theorem Nat.frequently_mod_eq {d n : ℕ} (h : d < n) :
∃ᶠ (m : ℕ) in Filter.atTop, m % n = d
source
theorem Nat.frequently_even :
∃ᶠ (m : ℕ) in Filter.atTop, Even m
source
theorem Nat.frequently_odd :
∃ᶠ (m : ℕ) in Filter.atTop, Odd m
source
theorem Filter.nonneg_of_eventually_pow_nonneg {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h : ∀ᶠ (n : ℕ) in atTop, 0 ≤ a ^ n) :
0 ≤ a