Documentation

Mathlib.Data.Nat.ModEq

Congruences modulo a natural number #

This file defines the equivalence relation a ≡ b [MOD n] on the natural numbers, and proves basic properties about it such as the Chinese Remainder Theorem modEq_and_modEq_iff_modEq_mul.

Notations #

a ≡ b [MOD n] is notation for nat.ModEq n a b, which is defined to mean a % n = b % n.

Tags #

ModEq, congruence, mod, MOD, modulo

def Nat.ModEq (n a b : ) :

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

Equations
    Instances For

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

      Equations
        Instances For
          instance Nat.instDecidableModEq {n a b : } :
          Equations
            theorem Nat.ModEq.refl {n : } (a : ) :
            a a [MOD n]
            theorem Nat.ModEq.rfl {n a : } :
            a a [MOD n]
            theorem Nat.ModEq.symm {n a b : } :
            a b [MOD n]b a [MOD n]
            theorem Nat.ModEq.trans {n a b c : } :
            a b [MOD n]b c [MOD n]a c [MOD n]
            Equations
              theorem Nat.ModEq.comm {n a b : } :
              a b [MOD n] b a [MOD n]
              theorem Nat.modEq_zero_iff_dvd {n a : } :
              a 0 [MOD n] n a
              theorem Dvd.dvd.modEq_zero_nat {n a : } (h : n a) :
              a 0 [MOD n]
              theorem Dvd.dvd.zero_modEq_nat {n a : } (h : n a) :
              0 a [MOD n]
              theorem Nat.modEq_iff_dvd {n a b : } :
              a b [MOD n] n b - a
              theorem Nat.ModEq.dvd {n a b : } :
              a b [MOD n]n b - a

              Alias of the forward direction of Nat.modEq_iff_dvd.

              theorem Nat.modEq_of_dvd {n a b : } :
              n b - aa b [MOD n]

              Alias of the reverse direction of Nat.modEq_iff_dvd.

              theorem Nat.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

              theorem Nat.mod_modEq (a n : ) :
              a % n a [MOD n]
              theorem Nat.ModEq.of_dvd {m n a b : } (d : m n) (h : a b [MOD n]) :
              a b [MOD m]
              theorem Nat.ModEq.mul_left' {n a b : } (c : ) (h : a b [MOD n]) :
              c * a c * b [MOD c * n]
              theorem Nat.ModEq.mul_left {n a b : } (c : ) (h : a b [MOD n]) :
              c * a c * b [MOD n]
              theorem Nat.ModEq.mul_right' {n a b : } (c : ) (h : a b [MOD n]) :
              a * c b * c [MOD n * c]
              theorem Nat.ModEq.mul_right {n a b : } (c : ) (h : a b [MOD n]) :
              a * c b * c [MOD n]
              theorem Nat.ModEq.mul {n a b c d : } (h₁ : a b [MOD n]) (h₂ : c d [MOD n]) :
              a * c b * d [MOD n]
              theorem Nat.ModEq.pow {n a b : } (m : ) (h : a b [MOD n]) :
              a ^ m b ^ m [MOD n]
              theorem Nat.ModEq.add {n a b c d : } (h₁ : a b [MOD n]) (h₂ : c d [MOD n]) :
              a + c b + d [MOD n]
              theorem Nat.ModEq.add_left {n a b : } (c : ) (h : a b [MOD n]) :
              c + a c + b [MOD n]
              theorem Nat.ModEq.add_right {n a b : } (c : ) (h : a b [MOD n]) :
              a + c b + c [MOD n]
              theorem Nat.ModEq.add_left_cancel {n a b c d : } (h₁ : a b [MOD n]) (h₂ : a + c b + d [MOD n]) :
              c d [MOD n]
              theorem Nat.ModEq.add_left_cancel' {n a b : } (c : ) (h : c + a c + b [MOD n]) :
              a b [MOD n]
              theorem Nat.ModEq.add_right_cancel {n a b c d : } (h₁ : c d [MOD n]) (h₂ : a + c b + d [MOD n]) :
              a b [MOD n]
              theorem Nat.ModEq.add_right_cancel' {n a b : } (c : ) (h : a + c b + c [MOD n]) :
              a b [MOD n]
              theorem Nat.ModEq.mul_left_cancel' {a b c m : } (hc : c 0) :
              c * a c * b [MOD c * m]a b [MOD m]

              Cancel left multiplication on both sides of the and in the modulus.

              For cancelling left multiplication in the modulus, see Nat.ModEq.of_mul_left.

              theorem Nat.ModEq.mul_left_cancel_iff' {a b c m : } (hc : c 0) :
              c * a c * b [MOD c * m] a b [MOD m]
              theorem Nat.ModEq.mul_right_cancel' {a b c m : } (hc : c 0) :
              a * c b * c [MOD m * c]a b [MOD m]

              Cancel right multiplication on both sides of the and in the modulus.

              For cancelling right multiplication in the modulus, see Nat.ModEq.of_mul_right.

              theorem Nat.ModEq.mul_right_cancel_iff' {a b c m : } (hc : c 0) :
              a * c b * c [MOD m * c] a b [MOD m]
              theorem Nat.ModEq.of_mul_left {n a b : } (m : ) (h : a b [MOD m * n]) :
              a b [MOD n]

              Cancel left multiplication in the modulus.

              For cancelling left multiplication on both sides of the , see nat.modeq.mul_left_cancel'.

              theorem Nat.ModEq.of_mul_right {n a b : } (m : ) :
              a b [MOD n * m]a b [MOD n]

              Cancel right multiplication in the modulus.

              For cancelling right multiplication on both sides of the , see nat.modeq.mul_right_cancel'.

              theorem Nat.ModEq.of_div {m a b c : } (h : a / c b / c [MOD m / c]) (ha : c a) :
              c bc ma b [MOD m]
              theorem Nat.modEq_sub {a b : } (h : b a) :
              a b [MOD a - b]
              theorem Nat.modEq_one {a b : } :
              a b [MOD 1]
              @[simp]
              theorem Nat.modEq_zero_iff {a b : } :
              a b [MOD 0] a = b
              @[simp]
              theorem Nat.add_modEq_left {n a : } :
              n + a a [MOD n]
              @[simp]
              theorem Nat.add_modEq_right {n a : } :
              a + n a [MOD n]
              theorem Nat.ModEq.le_of_lt_add {m a b : } (h1 : a b [MOD m]) (h2 : a < b + m) :
              a b
              theorem Nat.ModEq.add_le_of_lt {m a b : } (h1 : a b [MOD m]) (h2 : a < b) :
              a + m b
              theorem Nat.ModEq.dvd_iff {m a b d : } (h : a b [MOD m]) (hdm : d m) :
              d a d b
              theorem Nat.ModEq.gcd_eq {m a b : } (h : a b [MOD m]) :
              a.gcd m = b.gcd m
              theorem Nat.ModEq.eq_of_abs_lt {m a b : } (h : a b [MOD m]) (h2 : |b - a| < m) :
              a = b
              theorem Nat.ModEq.eq_of_lt_of_lt {m a b : } (h : a b [MOD m]) (ha : a < m) (hb : b < m) :
              a = b
              theorem Nat.ModEq.cancel_left_div_gcd {m a b c : } (hm : 0 < m) (h : c * a c * b [MOD m]) :
              a b [MOD m / m.gcd c]

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

              theorem Nat.ModEq.cancel_right_div_gcd {m a b c : } (hm : 0 < m) (h : a * c b * c [MOD m]) :
              a b [MOD m / m.gcd c]

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

              theorem Nat.ModEq.cancel_left_div_gcd' {m a b c d : } (hm : 0 < m) (hcd : c d [MOD m]) (h : c * a d * b [MOD m]) :
              a b [MOD m / m.gcd c]
              theorem Nat.ModEq.cancel_right_div_gcd' {m a b c d : } (hm : 0 < m) (hcd : c d [MOD m]) (h : a * c b * d [MOD m]) :
              a b [MOD m / m.gcd c]
              theorem Nat.ModEq.cancel_left_of_coprime {m a b c : } (hmc : m.gcd c = 1) (h : c * a c * b [MOD m]) :
              a b [MOD m]

              A common factor that's coprime with the modulus can be cancelled from a ModEq

              theorem Nat.ModEq.cancel_right_of_coprime {m a b c : } (hmc : m.gcd c = 1) (h : a * c b * c [MOD m]) :
              a b [MOD m]

              A common factor that's coprime with the modulus can be cancelled from a ModEq

              def Nat.chineseRemainder' {m n a b : } (h : a b [MOD n.gcd m]) :
              { k : // k a [MOD n] k b [MOD m] }

              The natural number less than lcm n m congruent to a mod n and b mod m

              Equations
                Instances For
                  def Nat.chineseRemainder {m n : } (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
                    Instances For
                      theorem Nat.chineseRemainder'_lt_lcm {m n a b : } (h : a b [MOD n.gcd m]) (hn : n 0) (hm : m 0) :
                      theorem Nat.chineseRemainder_lt_mul {m n : } (co : n.Coprime m) (a b : ) (hn : n 0) (hm : m 0) :
                      (chineseRemainder co a b) < n * m
                      theorem Nat.mod_lcm {m n a b : } (hn : a b [MOD n]) (hm : a b [MOD m]) :
                      a b [MOD n.lcm m]
                      theorem Nat.chineseRemainder_modEq_unique {m n : } (co : n.Coprime m) {a b z : } (hzan : z a [MOD n]) (hzbm : z b [MOD m]) :
                      z (chineseRemainder co a b) [MOD n * m]
                      theorem Nat.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]
                      theorem Nat.coprime_of_mul_modEq_one (b : ) {a n : } (h : a * b 1 [MOD n]) :
                      theorem Nat.add_mod_add_ite (a b c : ) :
                      ((a + b) % c + if c a % c + b % c then c else 0) = a % c + b % c
                      theorem Nat.add_mod_of_add_mod_lt {a b c : } (hc : a % c + b % c < c) :
                      (a + b) % c = a % c + b % c
                      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
                      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
                      theorem Nat.add_div_of_dvd_right {a b c : } (hca : c a) :
                      (a + b) / c = a / c + b / c
                      theorem Nat.add_div_of_dvd_left {a b c : } (hca : c b) :
                      (a + b) / c = a / c + b / c
                      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
                      theorem Nat.add_div_le_add_div (a b c : ) :
                      a / c + b / c (a + b) / c
                      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
                      theorem Nat.odd_mul_odd {n m : } :
                      n % 2 = 1m % 2 = 1n * m % 2 = 1
                      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
                      theorem Nat.odd_of_mod_four_eq_one {n : } :
                      n % 4 = 1n % 2 = 1
                      theorem Nat.odd_of_mod_four_eq_three {n : } :
                      n % 4 = 3n % 2 = 1
                      theorem Nat.odd_mod_four_iff {n : } :
                      n % 2 = 1 n % 4 = 1 n % 4 = 3

                      A natural number is odd iff it has residue 1 or 3 mod 4.

                      theorem Nat.mod_eq_of_modEq {a b n : } (h : a b [MOD n]) (hb : b < n) :
                      a % n = b