Documentation

Init.Data.Nat.Dvd

theorem Nat.dvd_refl (a : Nat) :
a a
theorem Nat.dvd_zero (a : Nat) :
a 0
theorem Nat.dvd_mul_left (a : Nat) (b : Nat) :
a b * a
theorem Nat.dvd_mul_right (a : Nat) (b : Nat) :
a a * b
theorem Nat.dvd_trans {a : Nat} {b : Nat} {c : Nat} (h₁ : a b) (h₂ : b c) :
a c
theorem Nat.eq_zero_of_zero_dvd {a : Nat} (h : 0 a) :
a = 0
@[simp]
theorem Nat.zero_dvd {n : Nat} :
0 n n = 0
theorem Nat.dvd_add {a : Nat} {b : Nat} {c : Nat} (h₁ : a b) (h₂ : a c) :
a b + c
theorem Nat.dvd_add_iff_right {k : Nat} {m : Nat} {n : Nat} (h : k m) :
k n k m + n
theorem Nat.dvd_add_iff_left {k : Nat} {m : Nat} {n : Nat} (h : k n) :
k m k m + n
theorem Nat.dvd_mod_iff {k : Nat} {m : Nat} {n : Nat} (h : k n) :
k m % n k m
theorem Nat.le_of_dvd {m : Nat} {n : Nat} (h : 0 < n) :
m nm n
theorem Nat.dvd_antisymm {m : Nat} {n : Nat} :
m nn mm = n
theorem Nat.pos_of_dvd_of_pos {m : Nat} {n : Nat} (H1 : m n) (H2 : 0 < n) :
0 < m
@[simp]
theorem Nat.one_dvd (n : Nat) :
1 n
theorem Nat.eq_one_of_dvd_one {n : Nat} (H : n 1) :
n = 1
theorem Nat.mod_eq_zero_of_dvd {m : Nat} {n : Nat} (H : m n) :
n % m = 0
theorem Nat.dvd_of_mod_eq_zero {m : Nat} {n : Nat} (H : n % m = 0) :
m n
theorem Nat.dvd_iff_mod_eq_zero {m : Nat} {n : Nat} :
m n n % m = 0
instance Nat.decidable_dvd :
DecidableRel fun (x1 x2 : Nat) => x1 x2
Equations
theorem Nat.emod_pos_of_not_dvd {a : Nat} {b : Nat} (h : ¬a b) :
0 < b % a
theorem Nat.mul_div_cancel' {n : Nat} {m : Nat} (H : n m) :
n * (m / n) = m
theorem Nat.div_mul_cancel {n : Nat} {m : Nat} (H : n m) :
m / n * n = m
@[simp]
theorem Nat.mod_mod_of_dvd {c : Nat} {b : Nat} (a : Nat) (h : c b) :
a % b % c = a % c
theorem Nat.dvd_of_mul_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : k * m k * n) :
m n
theorem Nat.dvd_of_mul_dvd_mul_right {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : m * k n * k) :
m n
theorem Nat.dvd_sub {k : Nat} {m : Nat} {n : Nat} (H : n m) (h₁ : k m) (h₂ : k n) :
k m - n
theorem Nat.mul_dvd_mul {a : Nat} {b : Nat} {c : Nat} {d : Nat} :
a bc da * c b * d
theorem Nat.mul_dvd_mul_left {b : Nat} {c : Nat} (a : Nat) (h : b c) :
a * b a * c
theorem Nat.mul_dvd_mul_right {a : Nat} {b : Nat} (h : a b) (c : Nat) :
a * c b * c
@[simp]
theorem Nat.dvd_one {n : Nat} :
n 1 n = 1
theorem Nat.mul_div_assoc {k : Nat} {n : Nat} (m : Nat) (H : k n) :
m * n / k = m * (n / k)