mathlib documentation

data.int.modeq

source
def int.modeq (n a b : ℤ) :
Prop

Equations
source
theorem int.modeq.refl {n : ℤ} (a : ℤ) :
a ≡ a [ZMOD n]

source
theorem int.modeq.symm {n a b : ℤ} (a_1 : a ≡ b [ZMOD n]) :
b ≡ a [ZMOD n]

source
theorem int.modeq.trans {n a b c : ℤ} (a_1 : a ≡ b [ZMOD n]) (a_2 : b ≡ c [ZMOD n]) :
a ≡ c [ZMOD n]

source
theorem int.modeq.coe_nat_modeq_iff {a b n : ℕ} :
↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]

source
@[instance]
def int.modeq.decidable {n a b : ℤ} :
decidable a ≡ b [ZMOD n]

Equations
source
theorem int.modeq.modeq_zero_iff {n a : ℤ} :
a ≡ 0 [ZMOD n] ↔ n ∣ a

source
theorem int.modeq.modeq_iff_dvd {n a b : ℤ} :
a ≡ b [ZMOD n] ↔ n ∣ b - a

source
theorem int.modeq.modeq_of_dvd_of_modeq {n m a b : ℤ} (d : m ∣ n) (h : a ≡ b [ZMOD n]) :
a ≡ b [ZMOD m]

source
theorem int.modeq.modeq_mul_left' {n a b c : ℤ} (hc : 0 ≤ c) (h : a ≡ b [ZMOD n]) :
c * a ≡ c * b [ZMOD c * n]

source
theorem int.modeq.modeq_mul_right' {n a b c : ℤ} (hc : 0 ≤ c) (h : a ≡ b [ZMOD n]) :
a * c ≡ b * c [ZMOD n * c]

source
theorem int.modeq.modeq_add {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) :
a + c ≡ b + d [ZMOD n]

source
theorem int.modeq.modeq_add_cancel_left {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) :
c ≡ d [ZMOD n]

source
theorem int.modeq.modeq_add_cancel_right {n a b c d : ℤ} (h₁ : c ≡ d [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) :
a ≡ b [ZMOD n]

source
theorem int.modeq.mod_modeq (a n : ℤ) :
a % n ≡ a [ZMOD n]

source
theorem int.modeq.modeq_neg {n a b : ℤ} (h : a ≡ b [ZMOD n]) :
-a ≡ -b [ZMOD n]

source
theorem int.modeq.modeq_sub {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) :
a - c ≡ b - d [ZMOD n]

source
theorem int.modeq.modeq_mul_left {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :
c * a ≡ c * b [ZMOD n]

source
theorem int.modeq.modeq_mul_right {n a b : ℤ} (c : ℤ) (h : a ≡ b [ZMOD n]) :
a * c ≡ b * c [ZMOD n]

source
theorem int.modeq.modeq_mul {n a b c d : ℤ} (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) :
a * c ≡ b * d [ZMOD n]

source
theorem int.modeq.modeq_of_modeq_mul_left {n a b : ℤ} (m : ℤ) (h : a ≡ b [ZMOD m * n]) :
a ≡ b [ZMOD n]

source
theorem int.modeq.modeq_of_modeq_mul_right {n a b : ℤ} (m : ℤ) (a_1 : a ≡ b [ZMOD n * m]) :
a ≡ b [ZMOD n]

source
theorem int.modeq.modeq_and_modeq_iff_modeq_mul {a b m n : ℤ} (hmn : m.nat_abs.coprime n.nat_abs) :
a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

source
theorem int.modeq.gcd_a_modeq (a b : ℕ) :
(↑a) * a.gcd_a b ≡ ↑(a.gcd b) [ZMOD ↑b]

source
theorem int.modeq.modeq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) :
a + n * c ≡ b [ZMOD n]

source
theorem int.modeq.mod_coprime {a b : ℕ} (hab : a.coprime b) :
∃ (y : ℤ), (↑a) * y ≡ 1 [ZMOD ↑b]

source
theorem int.modeq.exists_unique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) :
∃ (z : ℤ), 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b]

source
theorem int.modeq.exists_unique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) :
∃ (z : ℕ), ↑z < b ∧ ↑z ≡ a [ZMOD b]

source
@[simp]
theorem int.mod_mul_right_mod (a b c : ℤ) :
a % b * c % b = a % b

source
@[simp]
theorem int.mod_mul_left_mod (a b c : ℤ) :
a % b * c % c = a % c