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.

Equations

• n.ModEq a b = (a % n = b % n)

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

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

Equations

• One or more equations did not get rendered due to their size.

instance Int.instDecidableModEq {n : ℤ} {a : ℤ} {b : ℤ} : Decidable (n.ModEq a b)

Equations

• Int.instDecidableModEq = decEq (a % n) (b % n)

@[simp]

theorem Int.ModEq.refl {n : ℤ} (a : ℤ) : n.ModEq a a

theorem Int.ModEq.rfl {n : ℤ} {a : ℤ} : n.ModEq a a

instance Int.ModEq.instIsRefl {n : ℤ} : IsRefl ℤ n.ModEq

Equations

• ⋯ = ⋯

theorem Int.ModEq.symm {n : ℤ} {a : ℤ} {b : ℤ} : n.ModEq a b → n.ModEq b a

theorem Int.ModEq.trans {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} : n.ModEq a b → n.ModEq b c → n.ModEq a c

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

Equations

• ⋯ = ⋯

theorem Int.ModEq.eq {n : ℤ} {a : ℤ} {b : ℤ} : n.ModEq a b → a % n = b % n

theorem Int.modEq_comm {n : ℤ} {a : ℤ} {b : ℤ} : n.ModEq a b ↔ n.ModEq b a

theorem Int.natCast_modEq_iff {a : ℕ} {b : ℕ} {n : ℕ} : (↑n).ModEq ↑a ↑b ↔ n.ModEq a b

theorem Int.modEq_zero_iff_dvd {n : ℤ} {a : ℤ} : n.ModEq a 0 ↔ n ∣ a

theorem Dvd.dvd.modEq_zero_int {n : ℤ} {a : ℤ} (h : n ∣ a) : n.ModEq a 0

theorem Dvd.dvd.zero_modEq_int {n : ℤ} {a : ℤ} (h : n ∣ a) : n.ModEq 0 a

theorem Int.modEq_iff_dvd {n : ℤ} {a : ℤ} {b : ℤ} : n.ModEq a b ↔ n ∣ b - a

theorem Int.modEq_iff_add_fac {a : ℤ} {b : ℤ} {n : ℤ} : n.ModEq a b ↔ ∃ (t : ℤ), b = a + n * t

theorem Int.modEq_of_dvd {n : ℤ} {a : ℤ} {b : ℤ} : n ∣ b - a → n.ModEq a b

Alias of the reverse direction of Int.modEq_iff_dvd.

theorem Int.ModEq.dvd {n : ℤ} {a : ℤ} {b : ℤ} : n.ModEq a b → n ∣ b - a

Alias of the forward direction of Int.modEq_iff_dvd.

theorem Int.mod_modEq (a : ℤ) (n : ℤ) : n.ModEq (a % n) a

@[simp]

theorem Int.neg_modEq_neg {n : ℤ} {a : ℤ} {b : ℤ} : n.ModEq (-a) (-b) ↔ n.ModEq a b

@[simp]

theorem Int.modEq_neg {n : ℤ} {a : ℤ} {b : ℤ} : (-n).ModEq a b ↔ n.ModEq a b

theorem Int.ModEq.of_dvd {m : ℤ} {n : ℤ} {a : ℤ} {b : ℤ} (d : m ∣ n) (h : n.ModEq a b) : m.ModEq a b

theorem Int.ModEq.mul_left' {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} (h : n.ModEq a b) : (c * n).ModEq (c * a) (c * b)

theorem Int.ModEq.mul_right' {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} (h : n.ModEq a b) : (n * c).ModEq (a * c) (b * c)

theorem Int.ModEq.add {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (h₁ : n.ModEq a b) (h₂ : n.ModEq c d) : n.ModEq (a + c) (b + d)

theorem Int.ModEq.add_left {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq a b) : n.ModEq (c + a) (c + b)

theorem Int.ModEq.add_right {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq a b) : n.ModEq (a + c) (b + c)

theorem Int.ModEq.add_left_cancel {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (h₁ : n.ModEq a b) (h₂ : n.ModEq (a + c) (b + d)) : n.ModEq c d

theorem Int.ModEq.add_left_cancel' {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq (c + a) (c + b)) : n.ModEq a b

theorem Int.ModEq.add_right_cancel {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (h₁ : n.ModEq c d) (h₂ : n.ModEq (a + c) (b + d)) : n.ModEq a b

theorem Int.ModEq.add_right_cancel' {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq (a + c) (b + c)) : n.ModEq a b

theorem Int.ModEq.neg {n : ℤ} {a : ℤ} {b : ℤ} (h : n.ModEq a b) : n.ModEq (-a) (-b)

theorem Int.ModEq.sub {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (h₁ : n.ModEq a b) (h₂ : n.ModEq c d) : n.ModEq (a - c) (b - d)

theorem Int.ModEq.sub_left {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq a b) : n.ModEq (c - a) (c - b)

theorem Int.ModEq.sub_right {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq a b) : n.ModEq (a - c) (b - c)

theorem Int.ModEq.mul_left {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq a b) : n.ModEq (c * a) (c * b)

theorem Int.ModEq.mul_right {n : ℤ} {a : ℤ} {b : ℤ} (c : ℤ) (h : n.ModEq a b) : n.ModEq (a * c) (b * c)

theorem Int.ModEq.mul {n : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (h₁ : n.ModEq a b) (h₂ : n.ModEq c d) : n.ModEq (a * c) (b * d)

theorem Int.ModEq.pow {n : ℤ} {a : ℤ} {b : ℤ} (m : ℕ) (h : n.ModEq a b) : n.ModEq (a ^ m) (b ^ m)

theorem Int.ModEq.of_mul_left {n : ℤ} {a : ℤ} {b : ℤ} (m : ℤ) (h : (m * n).ModEq a b) : n.ModEq a b

theorem Int.ModEq.of_mul_right {n : ℤ} {a : ℤ} {b : ℤ} (m : ℤ) : (n * m).ModEq a b → n.ModEq a b

theorem Int.ModEq.cancel_right_div_gcd {m : ℤ} {a : ℤ} {b : ℤ} {c : ℤ} (hm : 0 < m) (h : m.ModEq (a * c) (b * c)) : (m / ↑(m.gcd c)).ModEq a b

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 : m.ModEq (c * a) (c * b)) : (m / ↑(m.gcd c)).ModEq a b

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 : (m / c).ModEq (a / c) (b / c)) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) : m.ModEq a b

theorem Int.modEq_one {a : ℤ} {b : ℤ} : a ≡ b [ZMOD 1]

theorem Int.modEq_sub (a : ℤ) (b : ℤ) : (a - b).ModEq 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.ModEq (n + a) a

@[simp]

theorem Int.add_modEq_right {n : ℤ} {a : ℤ} : n.ModEq (a + n) a

theorem Int.modEq_and_modEq_iff_modEq_mul {a : ℤ} {b : ℤ} {m : ℤ} {n : ℤ} (hmn : m.natAbs.Coprime n.natAbs) : m.ModEq a b ∧ n.ModEq a b ↔ (m * n).ModEq a b

theorem Int.gcd_a_modEq (a : ℕ) (b : ℕ) : (↑b).ModEq (↑a * a.gcdA b) ↑(a.gcd b)

theorem Int.modEq_add_fac {a : ℤ} {b : ℤ} {n : ℤ} (c : ℤ) (ha : n.ModEq a b) : n.ModEq (a + n * c) b

theorem Int.modEq_sub_fac {a : ℤ} {b : ℤ} {n : ℤ} (c : ℤ) (ha : n.ModEq a b) : n.ModEq (a - n * c) b

theorem Int.modEq_add_fac_self {a : ℤ} {t : ℤ} {n : ℤ} : n.ModEq (a + n * t) a

theorem Int.mod_coprime {a : ℕ} {b : ℕ} (hab : a.Coprime b) : ∃ (y : ℤ), (↑b).ModEq (↑a * y) 1

theorem Int.exists_unique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ (z : ℤ), 0 ≤ z ∧ z < b ∧ b.ModEq z a

theorem Int.exists_unique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ (z : ℕ), ↑z < b ∧ b.ModEq (↑z) a

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

@[deprecated Int.natCast_modEq_iff]

theorem Int.coe_nat_modEq_iff {a : ℕ} {b : ℕ} {n : ℕ} : (↑n).ModEq ↑a ↑b ↔ n.ModEq a b

Alias of Int.natCast_modEq_iff.