mathlib3 documentation

data.nat.modeq

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 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

a ≡ b [MOD n] = (a % n = b % n)

Instances for nat.modeq

@[protected, instance]

def nat.modeq.decidable (n a b : ℕ) :

decidable a ≡ b [MOD n]

@[protected, refl]

theorem nat.modeq.refl {n : ℕ} (a : ℕ) :

a ≡ a [MOD n]

@[protected]

theorem nat.modeq.rfl {n a : ℕ} :

a ≡ a [MOD n]

@[protected, instance]

def nat.modeq.is_refl {n : ℕ} :

is_refl ℕ n.modeq

@[protected, symm]

theorem nat.modeq.symm {n a b : ℕ} :

a ≡ b [MOD n] → b ≡ a [MOD n]

@[protected, trans]

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

theorem nat.modeq_of_dvd {n a b : ℕ} :

↑n ∣ ↑b - ↑a → a ≡ b [MOD n]

Alias of the reverse direction of nat.modeq_iff_dvd.

theorem nat.modeq.dvd {n a b : ℕ} :

a ≡ b [MOD n] → ↑n ∣ ↑b - ↑a

Alias of the forward direction of nat.modeq_iff_dvd.

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.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]

Cancel left multiplication on both sides of the ≡ and in the modulus.

For cancelling left multiplication in the modulus, see nat.modeq.of_mul_left.

@[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]

Cancel right multiplication on both sides of the ≡ and in the modulus.

For cancelling right multiplication in the modulus, see nat.modeq.of_mul_right.

@[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_mul_left {n a b : ℕ} (m : ℕ) (h : a ≡ b [MOD m * n]) :

a ≡ b [MOD n]

Cancel left multiplication in the modulus.

For cancelling left multiplication on both sides of the ≡, see nat.modeq.mul_left_cancel'.

theorem nat.modeq.of_mul_right {n a b : ℕ} (m : ℕ) :

a ≡ b [MOD n * m] → a ≡ b [MOD n]

Cancel right multiplication in the modulus.

For cancelling right multiplication on both sides of the ≡, see nat.modeq.mul_right_cancel'.

theorem nat.modeq.of_div {m a b c : ℕ} (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) (ha_1 : c ∣ b) (ha_2 : c ∣ m) :

a ≡ b [MOD m]

theorem nat.modeq_sub {a b : ℕ} (h : b ≤ a) :

a ≡ b [MOD a - b]

theorem nat.modeq_one {a b : ℕ} :

a ≡ b [MOD 1]

@[simp]

theorem nat.modeq_zero_iff {a b : ℕ} :

a ≡ b [MOD 0] ↔ a = b

@[simp]

theorem nat.add_modeq_left {n a : ℕ} :

n + a ≡ a [MOD n]

@[simp]

theorem nat.add_modeq_right {n a : ℕ} :

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 {m a b d : ℕ} (h : a ≡ b [MOD m]) (hdm : d ∣ m) :

d ∣ a ↔ d ∣ b

theorem nat.modeq.gcd_eq {m a b : ℕ} (h : a ≡ b [MOD m]) :

a.gcd m = b.gcd m

theorem nat.modeq.eq_of_abs_lt {m a b : ℕ} (h : a ≡ b [MOD m]) (h2 : |↑b - ↑a| < ↑m) :

a = b

theorem nat.modeq.eq_of_lt_of_lt {m a b : ℕ} (h : a ≡ b [MOD m]) (ha : a < m) (hb : b < m) :

a = b

theorem nat.modeq.cancel_left_div_gcd {m a b c : ℕ} (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.cancel_right_div_gcd {m a b c : ℕ} (hm : 0 < m) (h : a * c ≡ b * c [MOD m]) :

a ≡ b [MOD m / m.gcd c]

theorem nat.modeq.cancel_left_div_gcd' {m a b c d : ℕ} (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.cancel_right_div_gcd' {m a b c d : ℕ} (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.cancel_left_of_coprime {m a b c : ℕ} (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.cancel_right_of_coprime {m a b c : ℕ} (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

nat.chinese_remainder' h = dite (n = 0) (λ (hn : n = 0), ⟨a, _⟩) (λ (hn : ¬n = 0), dite (m = 0) (λ (hm : m = 0), ⟨b, _⟩) (λ (hm : ¬m = 0), ⟨nat.chinese_remainder'._match_1 (n.xgcd m), _⟩))
nat.chinese_remainder'._match_1 (c, d) = ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).to_nat

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

nat.chinese_remainder co a b = nat.chinese_remainder' _

theorem nat.chinese_remainder'_lt_lcm {m n a b : ℕ} (h : a ≡ b [MOD n.gcd m]) (hn : n ≠ 0) (hm : m ≠ 0) :

↑(nat.chinese_remainder' h) < n.lcm m

theorem nat.chinese_remainder_lt_mul {m n : ℕ} (co : n.coprime m) (a b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) :

↑(nat.chinese_remainder co a b) < n * m

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 = 1 → m % 2 = 1 → n * 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 = 1 → n % 2 = 1

theorem nat.odd_of_mod_four_eq_three {n : ℕ} :

n % 4 = 3 → n % 2 = 1

theorem nat.odd_mod_four_iff {n : ℕ} :

n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3

A natural number is odd iff it has residue 1 or 3 mod 4