Documentation

Mathlib.Order.Filter.ModEq

Numbers are frequently ModEq to fixed numbers #

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

theorem Nat.frequently_modEq {n : } (h : n 0) (d : ) :
Filter.Frequently (fun m => m d [MOD n]) Filter.atTop

Infinitely many natural numbers are equal to d mod n.

theorem Nat.frequently_mod_eq {d : } {n : } (h : d < n) :
Filter.Frequently (fun m => m % n = d) Filter.atTop
theorem Nat.frequently_even :
Filter.Frequently (fun m => Even m) Filter.atTop
theorem Nat.frequently_odd :
Filter.Frequently (fun m => Odd m) Filter.atTop