# mathlibdocumentation

data.nat.modeq

def nat.modeq  :
→ Prop

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

Equations
@[instance]
def nat.modeq.decidable (n a b : ) :

theorem nat.modeq.refl {n : } (a : ) :
a a [MOD n]

theorem nat.modeq.symm {n a b : } :
a b [MOD n]b a [MOD n]

theorem nat.modeq.trans {n a b c : } :
a b [MOD n]b c [MOD n]a c [MOD n]

theorem nat.modeq.modeq_zero_iff {n a : } :
a 0 [MOD n] n a

theorem nat.modeq.modeq_iff_dvd {n a b : } :
a b [MOD n] n b - a

theorem nat.modeq.modeq_of_dvd {n a b : } :
n b - aa b [MOD n]

theorem nat.modeq.dvd_of_modeq {n a b : } :
a b [MOD n]n b - a

theorem nat.modeq.modeq_iff_dvd' {n a b : } :
a b(a b [MOD n] n b - a)

A variant of modeq_iff_dvd with nat divisibility

theorem nat.modeq.mod_modeq (a n : ) :
a % n a [MOD n]

theorem nat.modeq.modeq_of_dvd_of_modeq {n m a b : } :
m na b [MOD n]a b [MOD m]

theorem nat.modeq.modeq_mul_left' {n a b : } (c : ) :
a b [MOD n]c * a c * b [MOD c * n]

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

theorem nat.modeq.modeq_mul_right' {n a b : } (c : ) :
a b [MOD n]a * c b * c [MOD n * c]

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

theorem nat.modeq.modeq_mul {n a b c d : } :
a b [MOD n]c d [MOD n]a * c b * d [MOD n]

theorem nat.modeq.modeq_add {n a b c d : } :
a b [MOD n]c d [MOD n]a + c b + d [MOD n]

theorem nat.modeq.modeq_add_cancel_left {n a b c d : } :
a b [MOD n]a + c b + d [MOD n]c d [MOD n]

theorem nat.modeq.modeq_add_cancel_right {n a b c d : } :
c d [MOD n]a + c b + d [MOD n]a b [MOD n]

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

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

def nat.modeq.chinese_remainder {n m : } (co : n.coprime 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
theorem nat.modeq.modeq_and_modeq_iff_modeq_mul {a b m n : } :
m.coprime n(a b [MOD m] a b [MOD n] a b [MOD m * n])

theorem nat.modeq.coprime_of_mul_modeq_one (b : ) {a n : } :
a * b 1 [MOD n]a.coprime n

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

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

theorem nat.div_mod_eq_mod_mul_div (a b c : ) :
a / b % c = a % b * c / b

(a + b) % c + ite (c a % c + b % c) c 0 = a % c + b % c

a % c + b % c < c(a + b) % c = a % c + b % c

c a % c + b % c(a + b) % c + c = a % c + b % c

theorem nat.add_div {a b c : } :
0 < c(a + b) / c = a / c + b / c + ite (c a % c + b % c) 1 0

a % c + b % c < c(a + b) / c = a / c + b / c

c a % c + b % c0 < c(a + b) / c = a / c + b / c + 1

a / c + b / c (a + b) / c

c a + b¬c ac a % c + b % c

theorem nat.odd_mul_odd {n m : } :
n % 2 = 1m % 2 = 1n * m % 2 = 1

theorem nat.odd_mul_odd_div_two {m n : } :
m % 2 = 1n % 2 = 1m * n / 2 = m * (n / 2) + m / 2

theorem nat.odd_of_mod_four_eq_one {n : } :
n % 4 = 1n % 2 = 1

theorem nat.odd_of_mod_four_eq_three {n : } :
n % 4 = 3n % 2 = 1

theorem list.nth_rotate {α : Type u_1} {l : list α} {n m : } :
m < l.length(l.rotate n).nth m = l.nth ((m + n) % l.length)

theorem list.rotate_eq_self_iff_eq_repeat {α : Type u_1} [hα : nonempty α] {l : list α} :
(∀ (n : ), l.rotate n = l) ∃ (a : α), l =