mathlib3 documentation

order.filter.modeq

Numbers are frequently modeq to fixed numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.at_top, 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.at_top, m % n = d
source
theorem nat.frequently_even  :
∃ᶠ (m : ℕ) in filter.at_top, even m
source
theorem nat.frequently_odd  :
∃ᶠ (m : ℕ) in filter.at_top, odd m