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