Documentation

Mathlib.Order.Filter.AtTopBot.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.atTop, 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.atTop, m % n = d
theorem Nat.frequently_even :
∃ᶠ (m : ) in Filter.atTop, Even m
theorem Nat.frequently_odd :
∃ᶠ (m : ) in Filter.atTop, Odd m
theorem Filter.nonneg_of_eventually_pow_nonneg {α : Type u_1} [LinearOrderedRing α] {a : α} (h : ∀ᶠ (n : ) in Filter.atTop, 0 a ^ n) :
0 a