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 : ℤ) : Prop

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

def «term_≡_[ZMOD_]» : Lean.TrailingParserDescr

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

@[simp]

theorem AddCommGroup.modEq_iff_intModEq {a b z : ℤ} : a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]

@[deprecated AddCommGroup.modEq_iff_intModEq (since := "2026-01-13")]

theorem AddCommGroup.modEq_iff_int_modEq {a b z : ℤ} : a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]

Alias of AddCommGroup.modEq_iff_intModEq.

@[simp]

theorem AddCommGroup.intCast_modEq_intCast {G : Type u_1} [AddCommGroupWithOne G] [CharZero G] {a b z : ℤ} : ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]

@[simp]

theorem AddCommGroup.intCast_modEq_intCast' {G : Type u_1} [AddCommGroupWithOne G] [CharZero G] {a b : ℤ} {n : ℕ} : ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]

theorem AddCommGroup.ModEq.intCast {G : Type u_1} [AddCommGroupWithOne G] [CharZero G] {a b z : ℤ} : a ≡ b [PMOD z] → ↑a ≡ ↑b [PMOD ↑z]

Alias of the reverse direction of AddCommGroup.intCast_modEq_intCast.

theorem AddCommGroup.ModEq.of_intCast {G : Type u_1} [AddCommGroupWithOne G] [CharZero G] {a b z : ℤ} : ↑a ≡ ↑b [PMOD ↑z] → a ≡ b [PMOD z]

Alias of the forward direction of AddCommGroup.intCast_modEq_intCast.

@[implicit_reducible]

instance Int.instDecidableModEq {n a b : ℤ} : Decidable (a ≡ b [ZMOD n])

@[simp]

theorem Int.ModEq.refl {n : ℤ} (a : ℤ) : a ≡ a [ZMOD n]

theorem Int.ModEq.rfl {n a : ℤ} : a ≡ a [ZMOD n]

instance Int.ModEq.instRefl {n : ℤ} : Std.Refl n.ModEq

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]

instance Int.ModEq.instIsTrans {n : ℤ} : IsTrans ℤ n.ModEq

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]

@[simp]

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_of_dvd {n a b : ℤ} : n ∣ b - a → a ≡ 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]) : -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 ∣ b → c ∣ m → a ≡ b [ZMOD m]

theorem Int.ModEq.mul_left_cancel' {m a b c : ℤ} (hc : c ≠ 0) : c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m]

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

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

theorem Int.ModEq.mul_left_cancel_iff' {m a b c : ℤ} (hc : c ≠ 0) : c * a ≡ c * b [ZMOD c * m] ↔ a ≡ b [ZMOD m]

theorem Int.ModEq.mul_right_cancel' {m a b c : ℤ} (hc : c ≠ 0) : a * c ≡ b * c [ZMOD m * c] → a ≡ b [ZMOD m]

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

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

theorem Int.ModEq.mul_right_cancel_iff' {m a b c : ℤ} (hc : c ≠ 0) : a * c ≡ b * c [ZMOD m * c] ↔ a ≡ b [ZMOD m]

theorem Int.ModEq.dvd_iff {n a b : ℤ} (h : a ≡ b [ZMOD n]) : n ∣ a ↔ n ∣ b

@[simp]

theorem Int.modulus_modEq_zero {n : ℤ} : n ≡ 0 [ZMOD n]

@[simp]

theorem Int.modEq_abs {n a b : ℤ} : a ≡ b [ZMOD |n|] ↔ a ≡ b [ZMOD n]

theorem Int.modEq_natAbs {n a b : ℤ} : a ≡ b [ZMOD ↑n.natAbs] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.add_modEq_left_iff {n a b : ℤ} : a + b ≡ a [ZMOD n] ↔ n ∣ b

@[simp]

theorem Int.add_modEq_right_iff {n a b : ℤ} : a + b ≡ b [ZMOD n] ↔ n ∣ a

@[simp]

theorem Int.left_modEq_add_iff {n a b : ℤ} : a ≡ a + b [ZMOD n] ↔ n ∣ b

@[simp]

theorem Int.right_modEq_add_iff {n a b : ℤ} : b ≡ a + b [ZMOD n] ↔ n ∣ a

@[simp]

theorem Int.add_modulus_modEq_iff {n a b : ℤ} : a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.modulus_add_modEq_iff {n a b : ℤ} : n + a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.modEq_add_modulus_iff {n a b : ℤ} : a ≡ b + n [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.modEq_modulus_add_iff {n a b : ℤ} : a ≡ n + b [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.add_mul_modulus_modEq_iff {n a b c : ℤ} : a + b * n ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

@[simp]

theorem Int.mul_modulus_add_modEq_iff {n a b c : ℤ} : b * n + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

@[simp]

theorem Int.modEq_add_mul_modulus_iff {n a b c : ℤ} : a ≡ b + c * n [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.modEq_mul_modulus_add_iff {n a b c : ℤ} : a ≡ b * n + c [ZMOD n] ↔ a ≡ c [ZMOD n]

@[simp]

theorem Int.add_modulus_mul_modEq_iff {n a b c : ℤ} : a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

@[simp]

theorem Int.modulus_mul_add_modEq_iff {n a b c : ℤ} : n * b + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

@[simp]

theorem Int.modEq_add_modulus_mul_iff {n a b c : ℤ} : a ≡ b + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.modEq_modulus_mul_add_iff {n a b c : ℤ} : a ≡ n * b + c [ZMOD n] ↔ a ≡ c [ZMOD n]

@[simp]

theorem Int.sub_modulus_modEq_iff {n a b : ℤ} : a - n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.sub_modulus_mul_modEq_iff {n a b c : ℤ} : a - n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

@[simp]

theorem Int.modEq_sub_modulus_iff {n a b : ℤ} : a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]

@[simp]

theorem Int.modEq_sub_modulus_mul_iff {n a b c : ℤ} : a ≡ b - n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

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

theorem Int.add_modEq_left {n a : ℤ} : n + a ≡ a [ZMOD n]

theorem Int.add_modEq_right {n a : ℤ} : a + n ≡ a [ZMOD n]

theorem Int.modEq_and_modEq_iff_modEq_lcm {a b m n : ℤ} : a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD ↑(m.lcm 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]

@[deprecated Int.add_modulus_mul_modEq_iff (since := "2025-10-16")]

theorem Int.modEq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n * c ≡ b [ZMOD n]

@[deprecated Int.sub_modulus_mul_modEq_iff (since := "2025-10-16")]

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]

theorem Int.existsUnique_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

theorem Int.ext_ediv_modEq {n a b : ℤ} (h0 : a / n = b / n) (h1 : a ≡ b [ZMOD n]) : a = b

theorem Int.ext_ediv_modEq_iff (n a b : ℤ) : a = b ↔ a / n = b / n ∧ a ≡ b [ZMOD n]

theorem Int.modEq_iff_eq_of_div_eq {n a b : ℤ} (h : a / n = b / n) : a ≡ b [ZMOD n] ↔ a = b