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

source
def Nat.ModEq (n : ℕ) (a : ℕ) (b : ℕ) :
Prop

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

Equations
Instances For
    source
    def Nat.«term_≡_[MOD_]» :
    Lean.TrailingParserDescr

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Nat.instDecidableModEq {n : ℕ} {a : ℕ} {b : ℕ} :
      Decidable (a ≡ b [MOD n])
      Equations
      • Nat.instDecidableModEq = decEq (a % n) (b % n)
      source
      theorem Nat.ModEq.refl {n : ℕ} (a : ℕ) :
      a ≡ a [MOD n]
      source
      theorem Nat.ModEq.rfl {n : ℕ} {a : ℕ} :
      a ≡ a [MOD n]
      source
      instance Nat.ModEq.instIsReflNatModEq {n : ℕ} :
      IsRefl ℕ (Nat.ModEq n)
      Equations
      • ⋯ = ⋯
      source
      theorem Nat.ModEq.symm {n : ℕ} {a : ℕ} {b : ℕ} :
      a ≡ b [MOD n] → b ≡ a [MOD n]
      source
      theorem Nat.ModEq.trans {n : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} :
      a ≡ b [MOD n] → b ≡ c [MOD n] → a ≡ c [MOD n]
      source
      instance Nat.ModEq.instTransNatModEq {n : ℕ} :
      Trans (Nat.ModEq n) (Nat.ModEq n) (Nat.ModEq n)
      Equations
      • Nat.ModEq.instTransNatModEq = { trans := ⋯ }
      source
      theorem Nat.ModEq.comm {n : ℕ} {a : ℕ} {b : ℕ} :
      a ≡ b [MOD n] ↔ b ≡ a [MOD n]
      source
      theorem Nat.modEq_zero_iff_dvd {n : ℕ} {a : ℕ} :
      a ≡ 0 [MOD n] ↔ n ∣ a
      source
      theorem Dvd.dvd.modEq_zero_nat {n : ℕ} {a : ℕ} (h : n ∣ a) :
      a ≡ 0 [MOD n]
      source
      theorem Dvd.dvd.zero_modEq_nat {n : ℕ} {a : ℕ} (h : n ∣ a) :
      0 ≡ a [MOD n]
      source
      theorem Nat.modEq_iff_dvd {n : ℕ} {a : ℕ} {b : ℕ} :
      a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a
      source
      theorem Nat.ModEq.dvd {n : ℕ} {a : ℕ} {b : ℕ} :
      a ≡ b [MOD n] → ↑n ∣ ↑b - ↑a

      Alias of the forward direction of Nat.modEq_iff_dvd.

      source
      theorem Nat.modEq_of_dvd {n : ℕ} {a : ℕ} {b : ℕ} :
      ↑n ∣ ↑b - ↑a → a ≡ b [MOD n]

      Alias of the reverse direction of Nat.modEq_iff_dvd.

      source
      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

      source
      theorem Nat.mod_modEq (a : ℕ) (n : ℕ) :
      a % n ≡ a [MOD n]
      source
      theorem Nat.ModEq.of_dvd {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (d : m ∣ n) (h : a ≡ b [MOD n]) :
      a ≡ b [MOD m]
      source
      theorem Nat.ModEq.mul_left' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
      c * a ≡ c * b [MOD c * n]
      source
      theorem Nat.ModEq.mul_left {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
      c * a ≡ c * b [MOD n]
      source
      theorem Nat.ModEq.mul_right' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
      a * c ≡ b * c [MOD n * c]
      source
      theorem Nat.ModEq.mul_right {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
      a * c ≡ b * c [MOD n]
      source
      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]
      source
      theorem Nat.ModEq.pow {n : ℕ} {a : ℕ} {b : ℕ} (m : ℕ) (h : a ≡ b [MOD n]) :
      a ^ m ≡ b ^ m [MOD n]
      source
      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]
      source
      theorem Nat.ModEq.add_left {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
      c + a ≡ c + b [MOD n]
      source
      theorem Nat.ModEq.add_right {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : a ≡ b [MOD n]) :
      a + c ≡ b + c [MOD n]
      source
      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]
      source
      theorem Nat.ModEq.add_left_cancel' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : c + a ≡ c + b [MOD n]) :
      a ≡ b [MOD n]
      source
      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]
      source
      theorem Nat.ModEq.add_right_cancel' {n : ℕ} {a : ℕ} {b : ℕ} (c : ℕ) (h : a + c ≡ b + c [MOD n]) :
      a ≡ b [MOD n]
      source
      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.

      source
      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]
      source
      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.

      source
      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]
      source
      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'.

      source
      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'.

      source
      theorem Nat.ModEq.of_div {m : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
      a ≡ b [MOD m]
      source
      theorem Nat.modEq_sub {a : ℕ} {b : ℕ} (h : b ≤ a) :
      a ≡ b [MOD a - b]
      source
      theorem Nat.modEq_one {a : ℕ} {b : ℕ} :
      a ≡ b [MOD 1]
      source
      @[simp]
      theorem Nat.modEq_zero_iff {a : ℕ} {b : ℕ} :
      a ≡ b [MOD 0] ↔ a = b
      source
      @[simp]
      theorem Nat.add_modEq_left {n : ℕ} {a : ℕ} :
      n + a ≡ a [MOD n]
      source
      @[simp]
      theorem Nat.add_modEq_right {n : ℕ} {a : ℕ} :
      a + n ≡ a [MOD n]
      source
      theorem Nat.ModEq.le_of_lt_add {m : ℕ} {a : ℕ} {b : ℕ} (h1 : a ≡ b [MOD m]) (h2 : a < b + m) :
      a ≤ b
      source
      theorem Nat.ModEq.add_le_of_lt {m : ℕ} {a : ℕ} {b : ℕ} (h1 : a ≡ b [MOD m]) (h2 : a < b) :
      a + m ≤ b
      source
      theorem Nat.ModEq.dvd_iff {m : ℕ} {a : ℕ} {b : ℕ} {d : ℕ} (h : a ≡ b [MOD m]) (hdm : d ∣ m) :
      d ∣ a ↔ d ∣ b
      source
      theorem Nat.ModEq.gcd_eq {m : ℕ} {a : ℕ} {b : ℕ} (h : a ≡ b [MOD m]) :
      Nat.gcd a m = Nat.gcd b m
      source
      theorem Nat.ModEq.eq_of_abs_lt {m : ℕ} {a : ℕ} {b : ℕ} (h : a ≡ b [MOD m]) (h2 : |↑b - ↑a| < ↑m) :
      a = b
      source
      theorem Nat.ModEq.eq_of_lt_of_lt {m : ℕ} {a : ℕ} {b : ℕ} (h : a ≡ b [MOD m]) (ha : a < m) (hb : b < m) :
      a = b
      source
      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 / Nat.gcd m c]

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

      source
      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 / Nat.gcd m c]

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

      source
      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 / Nat.gcd m c]
      source
      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 / Nat.gcd m c]
      source
      theorem Nat.ModEq.cancel_left_of_coprime {m : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} (hmc : Nat.gcd m 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

      source
      theorem Nat.ModEq.cancel_right_of_coprime {m : ℕ} {a : ℕ} {b : ℕ} {c : ℕ} (hmc : Nat.gcd m 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

      source
      def Nat.chineseRemainder' {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (h : a ≡ b [MOD Nat.gcd n 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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Nat.chineseRemainder {m : ℕ} {n : ℕ} (co : Nat.Coprime n 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
          source
          theorem Nat.chineseRemainder'_lt_lcm {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (h : a ≡ b [MOD Nat.gcd n m]) (hn : n ≠ 0) (hm : m ≠ 0) :
          ↑(Nat.chineseRemainder' h) < Nat.lcm n m
          source
          theorem Nat.chineseRemainder_lt_mul {m : ℕ} {n : ℕ} (co : Nat.Coprime n m) (a : ℕ) (b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) :
          ↑(Nat.chineseRemainder co a b) < n * m
          source
          theorem Nat.mod_lcm {m : ℕ} {n : ℕ} {a : ℕ} {b : ℕ} (hn : a ≡ b [MOD n]) (hm : a ≡ b [MOD m]) :
          a ≡ b [MOD Nat.lcm n m]
          source
          theorem Nat.chineseRemainder_modEq_unique {m : ℕ} {n : ℕ} (co : Nat.Coprime n m) {a : ℕ} {b : ℕ} {z : ℕ} (hzan : z ≡ a [MOD n]) (hzbm : z ≡ b [MOD m]) :
          z ≡ ↑(Nat.chineseRemainder co a b) [MOD n * m]
          source
          theorem Nat.modEq_and_modEq_iff_modEq_mul {a : ℕ} {b : ℕ} {m : ℕ} {n : ℕ} (hmn : Nat.Coprime m n) :
          a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n]
          source
          theorem Nat.coprime_of_mul_modEq_one (b : ℕ) {a : ℕ} {n : ℕ} (h : a * b ≡ 1 [MOD n]) :
          Nat.Coprime a n
          source
          theorem Nat.div_mod_eq_mod_mul_div (a : ℕ) (b : ℕ) (c : ℕ) :
          a / b % c = a % (b * c) / b
          source
          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
          source
          theorem Nat.add_mod_of_add_mod_lt {a : ℕ} {b : ℕ} {c : ℕ} (hc : a % c + b % c < c) :
          (a + b) % c = a % c + b % c
          source
          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
          source
          theorem Nat.add_div {a : ℕ} {b : ℕ} {c : ℕ} (hc0 : 0 < c) :
          (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0
          source
          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
          source
          theorem Nat.add_div_of_dvd_right {a : ℕ} {b : ℕ} {c : ℕ} (hca : c ∣ a) :
          (a + b) / c = a / c + b / c
          source
          theorem Nat.add_div_of_dvd_left {a : ℕ} {b : ℕ} {c : ℕ} (hca : c ∣ b) :
          (a + b) / c = a / c + b / c
          source
          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
          source
          theorem Nat.add_div_le_add_div (a : ℕ) (b : ℕ) (c : ℕ) :
          a / c + b / c ≤ (a + b) / c
          source
          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
          source
          theorem Nat.odd_mul_odd {n : ℕ} {m : ℕ} :
          n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1
          source
          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
          source
          theorem Nat.odd_of_mod_four_eq_one {n : ℕ} :
          n % 4 = 1 → n % 2 = 1
          source
          theorem Nat.odd_of_mod_four_eq_three {n : ℕ} :
          n % 4 = 3 → n % 2 = 1
          source
          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

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