Documentation

Mathlib.Data.Int.ModEq

Congruences modulo an integer #

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

def Int.ModEq (n : ) (a : ) (b : ) :

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

Equations
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance Int.instDecidableModEq {n : } {a : } {b : } :
      Equations
      • Int.instDecidableModEq = decEq (a % n) (b % n)
      @[simp]
      theorem Int.ModEq.refl {n : } (a : ) :
      a a [ZMOD n]
      theorem Int.ModEq.rfl {n : } {a : } :
      a a [ZMOD n]
      Equations
      • =
      theorem Int.ModEq.symm {n : } {a : } {b : } :
      a b [ZMOD n]b a [ZMOD n]
      theorem Int.ModEq.trans {n : } {a : } {b : } {c : } :
      a b [ZMOD n]b c [ZMOD n]a c [ZMOD n]
      Equations
      • =
      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 Dvd.dvd.modEq_zero_int {n : } {a : } (h : n a) :
      a 0 [ZMOD n]
      theorem 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_of_dvd {n : } {a : } {b : } :
      n b - aa b [ZMOD n]

      Alias of the reverse direction of Int.modEq_iff_dvd.

      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.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]
      theorem Int.ModEq.of_dvd {m : } {n : } {a : } {b : } (d : m n) (h : a b [ZMOD n]) :
      a b [ZMOD m]
      theorem Int.ModEq.mul_left' {n : } {a : } {b : } {c : } (h : a b [ZMOD n]) :
      c * a c * b [ZMOD c * n]
      theorem Int.ModEq.mul_right' {n : } {a : } {b : } {c : } (h : a b [ZMOD n]) :
      a * c b * c [ZMOD n * c]
      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]
      theorem Int.ModEq.add_left {n : } {a : } {b : } (c : ) (h : a b [ZMOD n]) :
      c + a c + b [ZMOD n]
      theorem Int.ModEq.add_right {n : } {a : } {b : } (c : ) (h : a b [ZMOD n]) :
      a + c b + c [ZMOD n]
      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]
      theorem Int.ModEq.add_left_cancel' {n : } {a : } {b : } (c : ) (h : c + a c + b [ZMOD n]) :
      a b [ZMOD n]
      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]
      theorem Int.ModEq.add_right_cancel' {n : } {a : } {b : } (c : ) (h : a + c b + c [ZMOD n]) :
      a b [ZMOD n]
      theorem Int.ModEq.neg {n : } {a : } {b : } (h : a b [ZMOD n]) :
      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]
      theorem Int.ModEq.sub_left {n : } {a : } {b : } (c : ) (h : a b [ZMOD n]) :
      c - a c - b [ZMOD n]
      theorem Int.ModEq.sub_right {n : } {a : } {b : } (c : ) (h : a b [ZMOD n]) :
      a - c b - c [ZMOD n]
      theorem Int.ModEq.mul_left {n : } {a : } {b : } (c : ) (h : a b [ZMOD n]) :
      c * a c * b [ZMOD n]
      theorem Int.ModEq.mul_right {n : } {a : } {b : } (c : ) (h : a b [ZMOD n]) :
      a * c b * c [ZMOD n]
      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]
      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 / (Int.gcd m 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 / (Int.gcd m 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 : c b) (ha : 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 : Nat.Coprime (Int.natAbs m) (Int.natAbs n)) :
      a b [ZMOD m] a b [ZMOD n] a b [ZMOD m * n]
      theorem Int.gcd_a_modEq (a : ) (b : ) :
      a * Nat.gcdA a b (Nat.gcd a 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_sub_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 : Nat.Coprime a 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]
      theorem Int.mod_mul_right_mod (a : ) (b : ) (c : ) :
      a % (b * c) % b = a % b
      theorem Int.mod_mul_left_mod (a : ) (b : ) (c : ) :
      a % (b * c) % c = a % c