mathlib docs: data.nat.modeq

nat.modeq.chinese_remainder co a b = ⟨nat.modeq.chinese_remainder._match_1 a b (n.xgcd m), _⟩
nat.modeq.chinese_remainder._match_1 a b (c, d) = ((↑b * c * ↑n + ↑a * d * ↑m) % (↑n * ↑m)).to_nat

source

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])

source

theorem nat.modeq.coprime_of_mul_modeq_one (b : ℕ) {a n : ℕ} :

a * b ≡ 1 [MOD n] → a.coprime n

source

@[simp]

theorem nat.mod_mul_right_mod (a b c : ℕ) :

a % (b * c) % b = a % b

source

@[simp]

theorem nat.mod_mul_left_mod (a b c : ℕ) :

a % (b * c) % c = a % c

source

theorem nat.div_mod_eq_mod_mul_div (a b c : ℕ) :

a / b % c = a % (b * c) / b

source

theorem nat.add_mod_add_ite (a b c : ℕ) :

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

source

theorem nat.add_mod_of_add_mod_lt {a b c : ℕ} :

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

source

theorem nat.add_mod_add_of_le_add_mod {a b c : ℕ} :

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

source

theorem nat.add_div {a b c : ℕ} :

0 < c → (a + b) / c = a / c + b / c + ite (c ≤ a % c + b % c) 1 0

source

theorem nat.add_div_eq_of_add_mod_lt {a b c : ℕ} :

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

source

theorem nat.add_div_eq_of_le_mod_add_mod {a b c : ℕ} :

c ≤ a % c + b % c → 0 < c → (a + b) / c = a / c + b / c + 1

source

theorem nat.add_div_le_add_div (a b c : ℕ) :

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

source

theorem nat.le_mod_add_mod_of_dvd_add_of_not_dvd {a b c : ℕ} :

c ∣ a + b → ¬c ∣ a → c ≤ a % c + b % c

source

theorem nat.odd_mul_odd {n m : ℕ} :

n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1

source

theorem nat.odd_mul_odd_div_two {m n : ℕ} :

m % 2 = 1 → n % 2 = 1 → m * n / 2 = m * (n / 2) + m / 2

source

theorem nat.odd_of_mod_four_eq_one {n : ℕ} :

n % 4 = 1 → n % 2 = 1

source

theorem nat.odd_of_mod_four_eq_three {n : ℕ} :

n % 4 = 3 → n % 2 = 1

source

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)

source

theorem list.rotate_eq_self_iff_eq_repeat {α : Type u_1} [hα : nonempty α] {l : list α} :

(∀ (n : ℕ), l.rotate n = l) ↔ ∃ (a : α), l = list.repeat a l.length

mathlib documentation

data.nat.modeq

General documentation

Additional documentation

Library

mathlib documentation

data.​nat.​modeq

General documentation

Additional documentation

Library

data.nat.modeq