mathlib documentation

data.int.modeq

def int.modeq  :
→ Prop

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

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

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]
def int.modeq.decidable {n a b : } :

Equations
theorem int.modeq.modeq_zero_iff {n a : } :
a 0 [ZMOD n] n a

theorem int.modeq.modeq_iff_dvd {n a b : } :
a b [ZMOD n] n b - a

theorem int.modeq.modeq_of_dvd_of_modeq {n m a b : } :
m na b [ZMOD n]a b [ZMOD m]

theorem int.modeq.modeq_mul_left' {n a b c : } :
0 ca b [ZMOD n]c * a c * b [ZMOD c * n]

theorem int.modeq.modeq_mul_right' {n a b c : } :
0 ca b [ZMOD n]a * c b * c [ZMOD n * c]

theorem int.modeq.modeq_add {n a b c d : } :
a b [ZMOD n]c d [ZMOD n]a + c b + d [ZMOD n]

theorem int.modeq.modeq_add_cancel_left {n a b c d : } :
a b [ZMOD n]a + c b + d [ZMOD n]c d [ZMOD n]

theorem int.modeq.modeq_add_cancel_right {n a b c d : } :
c d [ZMOD n]a + c b + d [ZMOD n]a b [ZMOD n]

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

theorem int.modeq.modeq_neg {n a b : } :
a b [ZMOD n]-a -b [ZMOD n]

theorem int.modeq.modeq_sub {n a b c d : } :
a b [ZMOD n]c d [ZMOD n]a - c b - d [ZMOD n]

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

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

theorem int.modeq.modeq_mul {n a b c d : } :
a b [ZMOD n]c d [ZMOD n]a * c b * d [ZMOD n]

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

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

theorem int.modeq.modeq_and_modeq_iff_modeq_mul {a b m n : } :
m.nat_abs.coprime n.nat_abs(a b [ZMOD m] a b [ZMOD n] a b [ZMOD m * n])

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

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

theorem int.modeq.mod_coprime {a b : } :
a.coprime b(∃ (y : ), (a) * y 1 [ZMOD b])

theorem int.modeq.exists_unique_equiv (a : ) {b : } :
0 < b(∃ (z : ), 0 z z < b z a [ZMOD b])

theorem int.modeq.exists_unique_equiv_nat (a : ) {b : } :
0 < b(∃ (z : ), z < b z a [ZMOD b])

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

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