Congruences modulo a natural number #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the equivalence relation
a ≡ b [MOD n] on the natural numbers,
and proves basic properties about it such as the Chinese Remainder Theorem
a ≡ b [MOD n] is notation for
nat.modeq n a b, which is defined to mean
a % n = b % n.
modeq, congruence, mod, MOD, modulo
The natural number less than
lcm n m congruent to