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
        Instances For
          instance Int.instDecidableModEq {n a b : } :
          Equations
            @[simp]
            theorem Int.ModEq.refl {n : } (a : ) :
            a a [ZMOD n]
            theorem Int.ModEq.rfl {n a : } :
            a a [ZMOD n]
            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]
            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.natCast_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.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 - aa 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]
            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 / (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) :
            c bc ma 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.natAbs.Coprime n.natAbs) :
            a b [ZMOD m] a b [ZMOD n] a b [ZMOD m * n]
            theorem Int.gcd_a_modEq (a b : ) :
            a * a.gcdA 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_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 : a.Coprime b) :
            (y : ), a * y 1 [ZMOD b]
            theorem Int.existsUnique_equiv (a : ) {b : } (hb : 0 < b) :
            (z : ), 0 z z < b z a [ZMOD b]
            @[deprecated Int.existsUnique_equiv (since := "2024-12-17")]
            theorem Int.exists_unique_equiv (a : ) {b : } (hb : 0 < b) :
            (z : ), 0 z z < b z a [ZMOD b]

            Alias of Int.existsUnique_equiv.

            theorem Int.existsUnique_equiv_nat (a : ) {b : } (hb : 0 < b) :
            (z : ), z < b z a [ZMOD b]
            @[deprecated Int.existsUnique_equiv_nat (since := "2024-12-17")]
            theorem Int.exists_unique_equiv_nat (a : ) {b : } (hb : 0 < b) :
            (z : ), z < b z a [ZMOD b]

            Alias of Int.existsUnique_equiv_nat.

            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