Congruences modulo a natural number #
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
modeq_and_modeq_iff_modeq_mul
.
Notations #
a ≡ b [MOD n]
is notation for nat.modeq n a b
, which is defined to mean a % n = b % n
.
Tags #
modeq, congruence, mod, MOD, modulo
The natural number less than n*m
congruent to a
mod n
and b
mod m
Equations
- nat.chinese_remainder co a b = nat.chinese_remainder' _
theorem
list.rotate_repeat
{α : Type u_1}
(a : α)
(n k : ℕ) :
(list.repeat a n).rotate k = list.repeat a n