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
Modular equality. n.ModEq a b
, or a ≡ b [MOD n]
, means that a - b
is a multiple of n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Nat.ModEq.instTrans = { trans := ⋯ }
Alias of the forward direction of Nat.modEq_iff_dvd
.
Alias of the reverse direction of Nat.modEq_iff_dvd
.
Cancel left multiplication in the modulus.
For cancelling left multiplication on both sides of the ≡
, see nat.modeq.mul_left_cancel'
.
Cancel right multiplication in the modulus.
For cancelling right multiplication on both sides of the ≡
, see nat.modeq.mul_right_cancel'
.
The natural number less than n*m
congruent to a
mod n
and b
mod m
Equations
- Nat.chineseRemainder co a b = Nat.chineseRemainder' ⋯