mathlib3 documentation

data.int.modeq

Congruences modulo an integer #

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 [ZMOD n] on the integers, similarly to how data.nat.modeq defines them for the natural numbers. The notation is short for n.modeq a b, which is defined to be a % n = b % n for integers a b n.

Tags #

modeq, congruence, mod, MOD, modulo, integers

@[protected, instance]

def int.modeq.decidable (n a b : ℤ) :

decidable a ≡ b [ZMOD n]

def int.modeq (n a b : ℤ) :

Prop

a ≡ b [ZMOD n] when a % n = b % n.

Equations

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

Instances for int.modeq

@[protected, refl]

theorem int.modeq.refl {n : ℤ} (a : ℤ) :

a ≡ a [ZMOD n]

@[protected]

theorem int.modeq.rfl {n a : ℤ} :

a ≡ a [ZMOD n]

@[protected, instance]

def int.modeq.is_refl {n : ℤ} :

is_refl ℤ n.modeq

@[protected, symm]

theorem int.modeq.symm {n a b : ℤ} :

a ≡ b [ZMOD n] → b ≡ a [ZMOD n]

@[protected, trans]

theorem int.modeq.trans {n a b c : ℤ} :

a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]

@[protected]

theorem int.modeq.eq {n a b : ℤ} :

a ≡ b [ZMOD n] → a % n = b % n

theorem int.modeq_comm {n a b : ℤ} :

a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n]

theorem int.coe_nat_modeq_iff {a b n : ℕ} :

↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]

theorem int.modeq_zero_iff_dvd {n a : ℤ} :

a ≡ 0 [ZMOD n] ↔ n ∣ a

theorem has_dvd.dvd.modeq_zero_int {n a : ℤ} (h : n ∣ a) :

a ≡ 0 [ZMOD n]

theorem has_dvd.dvd.zero_modeq_int {n a : ℤ} (h : n ∣ a) :

0 ≡ a [ZMOD n]

theorem int.modeq_iff_dvd {n a b : ℤ} :

a ≡ b [ZMOD n] ↔ n ∣ b - a

theorem int.modeq_iff_add_fac {a b n : ℤ} :

a ≡ b [ZMOD n] ↔ ∃ (t : ℤ), b = a + n * t

theorem int.modeq.dvd {n a b : ℤ} :

a ≡ b [ZMOD n] → n ∣ b - a

Alias of the forward direction of int.modeq_iff_dvd.

theorem int.modeq_of_dvd {n a b : ℤ} :

n ∣ b - a → a ≡ b [ZMOD n]

Alias of the reverse direction of int.modeq_iff_dvd.

theorem int.mod_modeq (a n : ℤ) :

a % n ≡ a [ZMOD n]

@[simp]

theorem int.neg_modeq_neg {n a b : ℤ} :

-a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem int.modeq_neg {n a b : ℤ} :

a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]

@[protected]

theorem int.modeq.of_dvd {m n a b : ℤ} (d : m ∣ n) (h : a ≡ b [ZMOD n]) :

a ≡ b [ZMOD m]

@[protected]

theorem int.modeq.mul_left' {n a b c : ℤ} (h : a ≡ b [ZMOD n]) :

c * a ≡ c * b [ZMOD c * n]

@[protected]

theorem int.modeq.mul_right' {n a b c : ℤ} (h : a ≡ b [ZMOD n]) :

a * c ≡ b * c [ZMOD n * c]

@[protected]

theorem int.modeq.add {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) :

a + c ≡ b + d [ZMOD n]

@[protected]

theorem int.modeq.add_left {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :

c + a ≡ c + b [ZMOD n]

@[protected]

theorem int.modeq.add_right {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :

a + c ≡ b + c [ZMOD n]

@[protected]

theorem int.modeq.add_left_cancel {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) :

c ≡ d [ZMOD n]

@[protected]

theorem int.modeq.add_left_cancel' {n a b : ℤ} (c : ℤ) (h : c + a ≡ c + b [ZMOD n]) :

a ≡ b [ZMOD n]

@[protected]

theorem int.modeq.add_right_cancel {n a b c d : ℤ} (h₁ : c ≡ d [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) :

a ≡ b [ZMOD n]

@[protected]

theorem int.modeq.add_right_cancel' {n a b : ℤ} (c : ℤ) (h : a + c ≡ b + c [ZMOD n]) :

a ≡ b [ZMOD n]

@[protected]

theorem int.modeq.neg {n a b : ℤ} (h : a ≡ b [ZMOD n]) :

-a ≡ -b [ZMOD n]

@[protected]

theorem int.modeq.sub {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) :

a - c ≡ b - d [ZMOD n]

@[protected]

theorem int.modeq.sub_left {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :

c - a ≡ c - b [ZMOD n]

@[protected]

theorem int.modeq.sub_right {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :

a - c ≡ b - c [ZMOD n]

@[protected]

theorem int.modeq.mul_left {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :

c * a ≡ c * b [ZMOD n]

@[protected]

theorem int.modeq.mul_right {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :

a * c ≡ b * c [ZMOD n]

@[protected]

theorem int.modeq.mul {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) :

a * c ≡ b * d [ZMOD n]

@[protected]

theorem int.modeq.pow {n a b : ℤ} (m : ℕ) (h : a ≡ b [ZMOD n]) :

a ^ m ≡ b ^ m [ZMOD n]

theorem int.modeq.of_mul_left {n a b : ℤ} (m : ℤ) (h : a ≡ b [ZMOD m * n]) :

a ≡ b [ZMOD n]

theorem int.modeq.of_mul_right {n a b : ℤ} (m : ℤ) :

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

theorem int.modeq.cancel_right_div_gcd {m a b c : ℤ} (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) :

a ≡ b [ZMOD m / ↑(m.gcd c)]

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

theorem int.modeq.cancel_left_div_gcd {m a b c : ℤ} (hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) :

a ≡ b [ZMOD m / ↑(m.gcd c)]

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

theorem int.modeq.of_div {m a b c : ℤ} (h : a / c ≡ b / c [ZMOD m / c]) (ha : c ∣ a) (ha_1 : c ∣ b) (ha_2 : c ∣ m) :

a ≡ b [ZMOD m]

theorem int.modeq_one {a b : ℤ} :

a ≡ b [ZMOD 1]

theorem int.modeq_sub (a b : ℤ) :

a ≡ b [ZMOD a - b]

@[simp]

theorem int.modeq_zero_iff {a b : ℤ} :

a ≡ b [ZMOD 0] ↔ a = b

@[simp]

theorem int.add_modeq_left {n a : ℤ} :

n + a ≡ a [ZMOD n]

@[simp]

theorem int.add_modeq_right {n a : ℤ} :

a + n ≡ a [ZMOD n]

theorem int.modeq_and_modeq_iff_modeq_mul {a b m n : ℤ} (hmn : m.nat_abs.coprime n.nat_abs) :

a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

theorem int.gcd_a_modeq (a b : ℕ) :

↑a * a.gcd_a b ≡ ↑(a.gcd b) [ZMOD ↑b]

theorem int.modeq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) :

a + n * c ≡ b [ZMOD n]

theorem int.modeq_add_fac_self {a t n : ℤ} :

a + n * t ≡ a [ZMOD n]

theorem int.mod_coprime {a b : ℕ} (hab : a.coprime b) :

∃ (y : ℤ), ↑a * y ≡ 1 [ZMOD ↑b]

theorem int.exists_unique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) :

∃ (z : ℤ), 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b]

theorem int.exists_unique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) :

∃ (z : ℕ), ↑z < b ∧ ↑z ≡ a [ZMOD b]

@[simp]

theorem int.mod_mul_right_mod (a b c : ℤ) :

a % (b * c) % b = a % b

@[simp]

theorem int.mod_mul_left_mod (a b c : ℤ) :

a % (b * c) % c = a % c