mathlib documentation

data.nat.modeq

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

def nat.modeq (n a b : ) :
Prop

Modular equality. n.modeq a b, or a ≡ b [MOD n], means that a - b is a multiple of n.

Equations
@[protected, instance]
def nat.modeq.decidable (n a b : ) :
@[protected]
theorem nat.modeq.refl {n : } (a : ) :
a a [MOD n]
@[protected]
theorem nat.modeq.rfl {n a : } :
a a [MOD n]
@[protected]
theorem nat.modeq.symm {n a b : } :
a b [MOD n]b a [MOD n]
@[protected]
theorem nat.modeq.trans {n a b c : } :
a b [MOD n]b c [MOD n]a c [MOD n]
@[protected]
theorem nat.modeq.comm {n a b : } :
a b [MOD n] b a [MOD n]
theorem nat.modeq_zero_iff_dvd {n a : } :
a 0 [MOD n] n a
theorem has_dvd.dvd.modeq_zero_nat {n a : } (h : n a) :
a 0 [MOD n]
theorem has_dvd.dvd.zero_modeq_nat {n a : } (h : n a) :
0 a [MOD n]
theorem nat.modeq_iff_dvd {n a b : } :
a b [MOD n] n b - a
@[protected]
theorem nat.modeq.dvd {n a b : } :
a b [MOD n]n b - a
theorem nat.modeq_of_dvd {n a b : } :
n b - aa b [MOD n]
theorem nat.modeq_iff_dvd' {n a b : } (h : a b) :
a b [MOD n] n b - a

A variant of modeq_iff_dvd with nat divisibility

theorem nat.mod_modeq (a n : ) :
a % n a [MOD n]
@[protected]
theorem nat.modeq.modeq_of_dvd {m n a b : } (d : m n) (h : a b [MOD n]) :
a b [MOD m]
@[protected]
theorem nat.modeq.mul_left' {n a b : } (c : ) (h : a b [MOD n]) :
c * a c * b [MOD c * n]
@[protected]
theorem nat.modeq.mul_left {n a b : } (c : ) (h : a b [MOD n]) :
c * a c * b [MOD n]
@[protected]
theorem nat.modeq.mul_right' {n a b : } (c : ) (h : a b [MOD n]) :
a * c b * c [MOD n * c]
@[protected]
theorem nat.modeq.mul_right {n a b : } (c : ) (h : a b [MOD n]) :
a * c b * c [MOD n]
@[protected]
theorem nat.modeq.mul {n a b c d : } (h₁ : a b [MOD n]) (h₂ : c d [MOD n]) :
a * c b * d [MOD n]
@[protected]
theorem nat.modeq.pow {n a b : } (m : ) (h : a b [MOD n]) :
a ^ m b ^ m [MOD n]
@[protected]
theorem nat.modeq.add {n a b c d : } (h₁ : a b [MOD n]) (h₂ : c d [MOD n]) :
a + c b + d [MOD n]
@[protected]
theorem nat.modeq.add_left {n a b : } (c : ) (h : a b [MOD n]) :
c + a c + b [MOD n]
@[protected]
theorem nat.modeq.add_right {n a b : } (c : ) (h : a b [MOD n]) :
a + c b + c [MOD n]
@[protected]
theorem nat.modeq.add_left_cancel {n a b c d : } (h₁ : a b [MOD n]) (h₂ : a + c b + d [MOD n]) :
c d [MOD n]
@[protected]
theorem nat.modeq.add_left_cancel' {n a b : } (c : ) (h : c + a c + b [MOD n]) :
a b [MOD n]
@[protected]
theorem nat.modeq.add_right_cancel {n a b c d : } (h₁ : c d [MOD n]) (h₂ : a + c b + d [MOD n]) :
a b [MOD n]
@[protected]
theorem nat.modeq.add_right_cancel' {n a b : } (c : ) (h : a + c b + c [MOD n]) :
a b [MOD n]
@[protected]
theorem nat.modeq.mul_left_cancel' {a b c m : } (hc : c 0) :
c * a c * b [MOD c * m]a b [MOD m]
@[protected]
theorem nat.modeq.mul_left_cancel_iff' {a b c m : } (hc : c 0) :
c * a c * b [MOD c * m] a b [MOD m]
@[protected]
theorem nat.modeq.mul_right_cancel' {a b c m : } (hc : c 0) :
a * c b * c [MOD m * c]a b [MOD m]
@[protected]
theorem nat.modeq.mul_right_cancel_iff' {a b c m : } (hc : c 0) :
a * c b * c [MOD m * c] a b [MOD m]
theorem nat.modeq.of_modeq_mul_left {n a b : } (m : ) (h : a b [MOD m * n]) :
a b [MOD n]
theorem nat.modeq.of_modeq_mul_right {n a b : } (m : ) :
a b [MOD n * m]a b [MOD n]
theorem nat.modeq_one {a b : } :
a b [MOD 1]
theorem nat.modeq_sub {a b : } (h : b a) :
a b [MOD a - b]
@[simp]
theorem nat.modeq_zero_iff {a b : } :
a b [MOD 0] a = b
@[simp]
theorem nat.add_modeq_left {a n : } :
n + a a [MOD n]
@[simp]
theorem nat.add_modeq_right {a n : } :
a + n a [MOD n]
theorem nat.modeq.le_of_lt_add {m a b : } (h1 : a b [MOD m]) (h2 : a < b + m) :
a b
theorem nat.modeq.add_le_of_lt {m a b : } (h1 : a b [MOD m]) (h2 : a < b) :
a + m b
theorem nat.modeq.dvd_iff_of_modeq_of_dvd {a b d m : } (h : a b [MOD m]) (hdm : d m) :
d a d b
theorem nat.modeq.gcd_eq_of_modeq {a b m : } (h : a b [MOD m]) :
a.gcd m = b.gcd m
theorem nat.modeq.eq_of_modeq_of_abs_lt {a b m : } (h : a b [MOD m]) (h2 : |b - a| < m) :
a = b
theorem nat.modeq.modeq_cancel_left_div_gcd {a b c m : } (hm : 0 < m) (h : c * a c * b [MOD m]) :
a b [MOD m / m.gcd c]

To cancel a common factor c from a modeq we must divide the modulus m by gcd m c

theorem nat.modeq.modeq_cancel_right_div_gcd {a b c m : } (hm : 0 < m) (h : a * c b * c [MOD m]) :
a b [MOD m / m.gcd c]
theorem nat.modeq.modeq_cancel_left_div_gcd' {a b c d m : } (hm : 0 < m) (hcd : c d [MOD m]) (h : c * a d * b [MOD m]) :
a b [MOD m / m.gcd c]
theorem nat.modeq.modeq_cancel_right_div_gcd' {a b c d m : } (hm : 0 < m) (hcd : c d [MOD m]) (h : a * c b * d [MOD m]) :
a b [MOD m / m.gcd c]
theorem nat.modeq.modeq_cancel_left_of_coprime {a b c m : } (hmc : m.gcd c = 1) (h : c * a c * b [MOD m]) :
a b [MOD m]

A common factor that's coprime with the modulus can be cancelled from a modeq

theorem nat.modeq.modeq_cancel_right_of_coprime {a b c m : } (hmc : m.gcd c = 1) (h : a * c b * c [MOD m]) :
a b [MOD m]

A common factor that's coprime with the modulus can be cancelled from a modeq

def nat.chinese_remainder' {m n a b : } (h : a b [MOD n.gcd m]) :
{k // k a [MOD n] k b [MOD m]}

The natural number less than lcm n m congruent to a mod n and b mod m

Equations
def nat.chinese_remainder {m n : } (co : n.coprime m) (a b : ) :
{k // k a [MOD n] k b [MOD m]}

The natural number less than n*m congruent to a mod n and b mod m

Equations
theorem nat.chinese_remainder'_lt_lcm {m n a b : } (h : a b [MOD n.gcd m]) (hn : n 0) (hm : m 0) :
theorem nat.chinese_remainder_lt_mul {m n : } (co : n.coprime m) (a b : ) (hn : n 0) (hm : m 0) :
theorem nat.modeq_and_modeq_iff_modeq_mul {a b m n : } (hmn : m.coprime n) :
a b [MOD m] a b [MOD n] a b [MOD m * n]
theorem nat.coprime_of_mul_modeq_one (b : ) {a n : } (h : a * b 1 [MOD n]) :
@[simp]
theorem nat.mod_mul_right_mod (a b c : ) :
a % b * c % b = a % b
@[simp]
theorem nat.mod_mul_left_mod (a b c : ) :
a % b * c % c = a % c
theorem nat.div_mod_eq_mod_mul_div (a b c : ) :
a / b % c = a % b * c / b
theorem nat.add_mod_add_ite (a b c : ) :
(a + b) % c + ite (c a % c + b % c) c 0 = a % c + b % c
theorem nat.add_mod_of_add_mod_lt {a b c : } (hc : a % c + b % c < c) :
(a + b) % c = a % c + b % c
theorem nat.add_mod_add_of_le_add_mod {a b c : } (hc : c a % c + b % c) :
(a + b) % c + c = a % c + b % c
theorem nat.add_div {a b c : } (hc0 : 0 < c) :
(a + b) / c = a / c + b / c + ite (c a % c + b % c) 1 0
theorem nat.add_div_eq_of_add_mod_lt {a b c : } (hc : a % c + b % c < c) :
(a + b) / c = a / c + b / c
@[protected]
theorem nat.add_div_of_dvd_right {a b c : } (hca : c a) :
(a + b) / c = a / c + b / c
@[protected]
theorem nat.add_div_of_dvd_left {a b c : } (hca : c b) :
(a + b) / c = a / c + b / c
theorem nat.add_div_eq_of_le_mod_add_mod {a b c : } (hc : c a % c + b % c) (hc0 : 0 < c) :
(a + b) / c = a / c + b / c + 1
theorem nat.add_div_le_add_div (a b c : ) :
a / c + b / c (a + b) / c
theorem nat.le_mod_add_mod_of_dvd_add_of_not_dvd {a b c : } (h : c a + b) (ha : ¬c a) :
c a % c + b % c
theorem nat.odd_mul_odd {n m : } :
n % 2 = 1m % 2 = 1n * m % 2 = 1
theorem nat.odd_mul_odd_div_two {m n : } (hm1 : m % 2 = 1) (hn1 : n % 2 = 1) :
m * n / 2 = m * (n / 2) + m / 2
theorem nat.odd_of_mod_four_eq_one {n : } :
n % 4 = 1n % 2 = 1
theorem nat.odd_of_mod_four_eq_three {n : } :
n % 4 = 3n % 2 = 1
theorem list.nth_rotate {α : Type u_1} {l : list α} {n m : } (hml : m < l.length) :
(l.rotate n).nth m = l.nth ((m + n) % l.length)
theorem list.rotate_eq_self_iff_eq_repeat {α : Type u_1} [hα : nonempty α] {l : list α} :
(∀ (n : ), l.rotate n = l) ∃ (a : α), l = list.repeat a l.length
theorem list.rotate_repeat {α : Type u_1} (a : α) (n k : ) :
theorem list.rotate_one_eq_self_iff_eq_repeat {α : Type u_1} [nonempty α] {l : list α} :
l.rotate 1 = l ∃ (a : α), l = list.repeat a l.length