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 : ) :
def int.modeq (n a b : ) :
Prop

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

Equations
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 : } :
@[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 : } :
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]) :
@[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