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 → ∞.

theorem nat.frequently_modeq {n : } (h : n 0) (d : ) :

Infinitely many natural numbers are equal to d mod n.

theorem nat.frequently_mod_eq {d n : } (h : d < n) :