mathlib documentation

data.nat.modeq

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

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

Equations
source
@[instance]
def nat.modeq.decidable (n a b : ℕ) :
decidable a ≡ b [MOD n]

source
theorem nat.modeq.refl {n : ℕ} (a : ℕ) :
a ≡ a [MOD n]

source
theorem nat.modeq.symm {n a b : ℕ} (a_1 : a ≡ b [MOD n]) :
b ≡ a [MOD n]

source
theorem nat.modeq.trans {n a b c : ℕ} (a_1 : a ≡ b [MOD n]) (a_2 : b ≡ c [MOD n]) :
a ≡ c [MOD n]

source
theorem nat.modeq.modeq_zero_iff {n a : ℕ} :
a ≡ 0 [MOD n] ↔ n ∣ a

source
theorem nat.modeq.modeq_iff_dvd {n a b : ℕ} :
a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a

source
theorem nat.modeq.modeq_of_dvd {n a b : ℕ} (a_1 : ↑n ∣ ↑b - ↑a) :
a ≡ b [MOD n]

source
theorem nat.modeq.dvd_of_modeq {n a b : ℕ} (a_1 : a ≡ b [MOD n]) :
↑n ∣ ↑b - ↑a

source
theorem nat.modeq.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

source
theorem nat.modeq.mod_modeq (a n : ℕ) :
a % n ≡ a [MOD n]

source
theorem nat.modeq.modeq_of_dvd_of_modeq {n m a b : ℕ} (d : m ∣ n) (h : a ≡ b [MOD n]) :
a ≡ b [MOD m]

source
theorem nat.modeq.modeq_mul_left' {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
c * a ≡ c * b [MOD c * n]

source
theorem nat.modeq.modeq_mul_left {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
c * a ≡ c * b [MOD n]

source
theorem nat.modeq.modeq_mul_right' {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
a * c ≡ b * c [MOD n * c]

source
theorem nat.modeq.modeq_mul_right {n a b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
a * c ≡ b * c [MOD n]

source
theorem nat.modeq.modeq_mul {n a b c d : ℕ} (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) :
a * c ≡ b * d [MOD n]

source
theorem nat.modeq.modeq_add {n a b c d : ℕ} (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) :
a + c ≡ b + d [MOD n]

source
theorem nat.modeq.modeq_add_cancel_left {n a b c d : ℕ} (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) :
c ≡ d [MOD n]

source
theorem nat.modeq.modeq_add_cancel_right {n a b c d : ℕ} (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) :
a ≡ b [MOD n]

source
theorem nat.modeq.modeq_of_modeq_mul_left {n a b : ℕ} (m : ℕ) (h : a ≡ b [MOD m * n]) :
a ≡ b [MOD n]

source
theorem nat.modeq.modeq_of_modeq_mul_right {n a b : ℕ} (m : ℕ) (a_1 : a ≡ b [MOD n * m]) :
a ≡ b [MOD n]

source
def nat.modeq.chinese_remainder {n m : ℕ} (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
source
theorem nat.modeq.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]

source
theorem nat.modeq.coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) :
a.coprime n

source
@[simp]
theorem nat.mod_mul_right_mod (a b c : ℕ) :
a % b * c % b = a % b

source
@[simp]
theorem nat.mod_mul_left_mod (a b c : ℕ) :
a % b * c % c = a % c

source
theorem nat.div_mod_eq_mod_mul_div (a b c : ℕ) :
a / b % c = a % b * c / b

source
theorem nat.add_mod_add_ite (a b c : ℕ) :
(a + b) % c + ite (c ≤ a % c + b % c) c 0 = a % c + b % c

source
theorem nat.add_mod_of_add_mod_lt {a b c : ℕ} (hc : a % c + b % c < c) :
(a + b) % c = a % c + b % c

source
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

source
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

source
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

source
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

source
theorem nat.add_div_le_add_div (a b c : ℕ) :
a / c + b / c ≤ (a + b) / c

source
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

source
theorem nat.odd_mul_odd {n m : ℕ} (hn1 : n % 2 = 1) (hm1 : m % 2 = 1) :
n * m % 2 = 1

source
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

source
theorem nat.odd_of_mod_four_eq_one {n : ℕ} (h : n % 4 = 1) :
n % 2 = 1

source
theorem nat.odd_of_mod_four_eq_three {n : ℕ} (h : n % 4 = 3) :
n % 2 = 1

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

source
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