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

• n.ModEq a b = (a % n = b % n)

def Nat.«term_≡_[MOD_]» : Lean.TrailingParserDescr

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.

instance Nat.instDecidableModEq {n : ℕ} {a : ℕ} {b : ℕ} : Decidable (n.ModEq a b)

Equations

• Nat.instDecidableModEq = decEq (a % n) (b % n)

theorem Nat.ModEq.refl {n : ℕ} (a : ℕ) : n.ModEq a a

theorem Nat.ModEq.rfl {n : ℕ} {a : ℕ} : n.ModEq a a

instance Nat.ModEq.instIsRefl {n : ℕ} : IsRefl ℕ n.ModEq

Equations

• ⋯ = ⋯

theorem Nat.ModEq.symm {n : ℕ} {a : ℕ} {b : ℕ} : n.ModEq a b → n.ModEq b a

theorem Nat.ModEq.trans {n : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} : n.ModEq a b → n.ModEq b c → n.ModEq a c

instance Nat.ModEq.instTrans {n : ℕ} : Trans n.ModEq n.ModEq n.ModEq

Equations

• Nat.ModEq.instTrans = { trans := ⋯ }

theorem Nat.ModEq.comm {n : ℕ} {a : ℕ} {b : ℕ} : n.ModEq a b ↔ n.ModEq b a

theorem Nat.modEq_zero_iff_dvd {n : ℕ} {a : ℕ} : n.ModEq a 0 ↔ n ∣ a

theorem Dvd.dvd.modEq_zero_nat {n : ℕ} {a : ℕ} (h : n ∣ a) : n.ModEq a 0

theorem Dvd.dvd.zero_modEq_nat {n : ℕ} {a : ℕ} (h : n ∣ a) : n.ModEq 0 a

theorem Nat.modEq_iff_dvd {n : ℕ} {a : ℕ} {b : ℕ} : n.ModEq a b ↔ ↑n ∣ ↑b - ↑a

theorem Nat.ModEq.dvd {n : ℕ} {a : ℕ} {b : ℕ} : n.ModEq a b → ↑n ∣ ↑b - ↑a

Alias of the forward direction of Nat.modEq_iff_dvd.

theorem Nat.modEq_of_dvd {n : ℕ} {a : ℕ} {b : ℕ} : ↑n ∣ ↑b - ↑a → n.ModEq a b

Alias of the reverse direction of Nat.modEq_iff_dvd.

theorem Nat.modEq_iff_dvd' {n : ℕ} {a : ℕ} {b : ℕ} (h : a ≤ b) : n.ModEq a b ↔ n ∣ b - a

A variant of modEq_iff_dvd with Nat divisibility

theorem Nat.mod_modEq (a : ℕ) (n : ℕ) : n.ModEq (a % n) a

theorem Nat.ModEq.of_dvd {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (d : m ∣ n) (h : n.ModEq a b) : m.ModEq a b

theorem Nat.ModEq.mul_left' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq a b) : (c * n).ModEq (c * a) (c * b)

theorem Nat.ModEq.mul_left {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq a b) : n.ModEq (c * a) (c * b)

theorem Nat.ModEq.mul_right' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq a b) : (n * c).ModEq (a * c) (b * c)

theorem Nat.ModEq.mul_right {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq a b) : n.ModEq (a * c) (b * c)

theorem Nat.ModEq.mul {n : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h₁ : n.ModEq a b) (h₂ : n.ModEq c d) : n.ModEq (a * c) (b * d)

theorem Nat.ModEq.pow {n : ℕ} {a : ℕ} {b : ℕ} (m : ℕ) (h : n.ModEq a b) : n.ModEq (a ^ m) (b ^ m)

theorem Nat.ModEq.add {n : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h₁ : n.ModEq a b) (h₂ : n.ModEq c d) : n.ModEq (a + c) (b + d)

theorem Nat.ModEq.add_left {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq a b) : n.ModEq (c + a) (c + b)

theorem Nat.ModEq.add_right {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq a b) : n.ModEq (a + c) (b + c)

theorem Nat.ModEq.add_left_cancel {n : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h₁ : n.ModEq a b) (h₂ : n.ModEq (a + c) (b + d)) : n.ModEq c d

theorem Nat.ModEq.add_left_cancel' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq (c + a) (c + b)) : n.ModEq a b

theorem Nat.ModEq.add_right_cancel {n : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h₁ : n.ModEq c d) (h₂ : n.ModEq (a + c) (b + d)) : n.ModEq a b

theorem Nat.ModEq.add_right_cancel' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : n.ModEq (a + c) (b + c)) : n.ModEq a b

theorem Nat.ModEq.mul_left_cancel' {a : ℕ} {b : ℕ} {c : ℕ} {m : ℕ} (hc : c ≠ 0) : (c * m).ModEq (c * a) (c * b) → m.ModEq a b

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.

theorem Nat.ModEq.mul_left_cancel_iff' {a : ℕ} {b : ℕ} {c : ℕ} {m : ℕ} (hc : c ≠ 0) : (c * m).ModEq (c * a) (c * b) ↔ m.ModEq a b

theorem Nat.ModEq.mul_right_cancel' {a : ℕ} {b : ℕ} {c : ℕ} {m : ℕ} (hc : c ≠ 0) : (m * c).ModEq (a * c) (b * c) → m.ModEq a b

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.

theorem Nat.ModEq.mul_right_cancel_iff' {a : ℕ} {b : ℕ} {c : ℕ} {m : ℕ} (hc : c ≠ 0) : (m * c).ModEq (a * c) (b * c) ↔ m.ModEq a b

theorem Nat.ModEq.of_mul_left {n : ℕ} {a : ℕ} {b : ℕ} (m : ℕ) (h : (m * n).ModEq a b) : n.ModEq a b

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 : ℕ) : (n * m).ModEq a b → n.ModEq a b

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 : (m / c).ModEq (a / c) (b / c)) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) : m.ModEq a b

theorem Nat.modEq_sub {a : ℕ} {b : ℕ} (h : b ≤ a) : (a - b).ModEq 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.ModEq (n + a) a

@[simp]

theorem Nat.add_modEq_right {n : ℕ} {a : ℕ} : n.ModEq (a + n) a

theorem Nat.ModEq.le_of_lt_add {m : ℕ} {a : ℕ} {b : ℕ} (h1 : m.ModEq a b) (h2 : a < b + m) : a ≤ b

theorem Nat.ModEq.add_le_of_lt {m : ℕ} {a : ℕ} {b : ℕ} (h1 : m.ModEq a b) (h2 : a < b) : a + m ≤ b

theorem Nat.ModEq.dvd_iff {m : ℕ} {a : ℕ} {b : ℕ} {d : ℕ} (h : m.ModEq a b) (hdm : d ∣ m) : d ∣ a ↔ d ∣ b

theorem Nat.ModEq.gcd_eq {m : ℕ} {a : ℕ} {b : ℕ} (h : m.ModEq a b) : a.gcd m = b.gcd m

theorem Nat.ModEq.eq_of_abs_lt {m : ℕ} {a : ℕ} {b : ℕ} (h : m.ModEq a b) (h2 : |↑b - ↑a| < ↑m) : a = b

theorem Nat.ModEq.eq_of_lt_of_lt {m : ℕ} {a : ℕ} {b : ℕ} (h : m.ModEq a b) (ha : a < m) (hb : b < m) : a = b

theorem Nat.ModEq.cancel_left_div_gcd {m : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} (hm : 0 < m) (h : m.ModEq (c * a) (c * b)) : (m / m.gcd c).ModEq a b

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 : m.ModEq (a * c) (b * c)) : (m / m.gcd c).ModEq a b

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

theorem Nat.ModEq.cancel_left_div_gcd' {m : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (hm : 0 < m) (hcd : m.ModEq c d) (h : m.ModEq (c * a) (d * b)) : (m / m.gcd c).ModEq a b

theorem Nat.ModEq.cancel_right_div_gcd' {m : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (hm : 0 < m) (hcd : m.ModEq c d) (h : m.ModEq (a * c) (b * d)) : (m / m.gcd c).ModEq a b

theorem Nat.ModEq.cancel_left_of_coprime {m : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} (hmc : m.gcd c = 1) (h : m.ModEq (c * a) (c * b)) : m.ModEq a b

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 : m.ModEq (a * c) (b * c)) : m.ModEq a b

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

def Nat.chineseRemainder' {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (h : (n.gcd m).ModEq a b) : { k : ℕ // n.ModEq k a ∧ m.ModEq k b }

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

Equations

• One or more equations did not get rendered due to their size.

def Nat.chineseRemainder {m : ℕ} {n : ℕ} (co : n.Coprime m) (a : ℕ) (b : ℕ) : { k : ℕ // n.ModEq k a ∧ m.ModEq k b }

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

Equations

• Nat.chineseRemainder co a b = Nat.chineseRemainder' ⋯

theorem Nat.chineseRemainder'_lt_lcm {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (h : (n.gcd m).ModEq a b) (hn : n ≠ 0) (hm : m ≠ 0) : ↑(Nat.chineseRemainder' h) < n.lcm m

theorem Nat.chineseRemainder_lt_mul {m : ℕ} {n : ℕ} (co : n.Coprime m) (a : ℕ) (b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) : ↑(Nat.chineseRemainder co a b) < n * m

theorem Nat.mod_lcm {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (hn : n.ModEq a b) (hm : m.ModEq a b) : (n.lcm m).ModEq a b

theorem Nat.chineseRemainder_modEq_unique {m : ℕ} {n : ℕ} (co : n.Coprime m) {a : ℕ} {b : ℕ} {z : ℕ} (hzan : n.ModEq z a) (hzbm : m.ModEq z b) : (n * m).ModEq z ↑(Nat.chineseRemainder co a b)

theorem Nat.modEq_and_modEq_iff_modEq_mul {a : ℕ} {b : ℕ} {m : ℕ} {n : ℕ} (hmn : m.Coprime n) : m.ModEq a b ∧ n.ModEq a b ↔ (m * n).ModEq a b

theorem Nat.coprime_of_mul_modEq_one (b : ℕ) {a : ℕ} {n : ℕ} (h : n.ModEq (a * b) 1) : a.Coprime n

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 + if c ≤ a % c + b % c then c else 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 + if c ≤ a % c + b % c then 1 else 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

theorem Nat.add_div_of_dvd_right {a : ℕ} {b : ℕ} {c : ℕ} (hca : c ∣ a) : (a + b) / c = a / c + b / c

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

theorem Nat.mod_eq_of_modEq {a : ℕ} {b : ℕ} {n : ℕ} (h : n.ModEq a b) (hb : b < n) : a % n = b