source
@[simp]
theorem Nat.dvd_refl (a : Nat) :
a ∣ a
source
@[simp]
theorem Nat.dvd_zero (a : Nat) :
a ∣ 0
source
theorem Nat.dvd_mul_left (a b : Nat) :
a ∣ b * a
source
theorem Nat.dvd_mul_right (a b : Nat) :
a ∣ a * b
source
theorem Nat.dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) :
a ∣ c
source
theorem Nat.dvd_mul_left_of_dvd {a b : Nat} (h : a ∣ b) (c : Nat) :
a ∣ c * b
source
theorem Nat.dvd_mul_right_of_dvd {a b : Nat} (h : a ∣ b) (c : Nat) :
a ∣ b * c
source
theorem Nat.eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) :
a = 0
source
@[simp]
theorem Nat.zero_dvd {n : Nat} :
0 ∣ n ↔ n = 0
source
theorem Nat.dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b + c
source
theorem Nat.dvd_add_iff_right {k m n : Nat} (h : k ∣ m) :
k ∣ n ↔ k ∣ m + n
source
theorem Nat.dvd_add_iff_left {k m n : Nat} (h : k ∣ n) :
k ∣ m ↔ k ∣ m + n
source
theorem Nat.dvd_mod_iff {k m n : Nat} (h : k ∣ n) :
k ∣ m % n ↔ k ∣ m
source
theorem Nat.le_of_dvd {m n : Nat} (h : 0 < n) :
m ∣ n → m ≤ n
source
theorem Nat.dvd_antisymm {m n : Nat} :
m ∣ n → n ∣ m → m = n
source
theorem Nat.pos_of_dvd_of_pos {m n : Nat} (H1 : m ∣ n) (H2 : 0 < n) :
0 < m
source
@[simp]
theorem Nat.one_dvd (n : Nat) :
1 ∣ n
source
theorem Nat.eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) :
n = 1
source
theorem Nat.mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) :
n % m = 0
source
theorem Nat.dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) :
m ∣ n
source
theorem Nat.dvd_iff_mod_eq_zero {m n : Nat} :
m ∣ n ↔ n % m = 0
source
instance Nat.decidable_dvd :
DecidableRel fun (x1 x2 : Nat) => x1 ∣ x2
Equations

- x✝¹.decidable_dvd x✝ = decidable_of_decidable_of_iff ⋯

source
theorem Nat.emod_pos_of_not_dvd {a b : Nat} (h : ¬a ∣ b) :
0 < b % a
source
theorem Nat.mul_div_cancel' {n m : Nat} (H : n ∣ m) :
n * (m / n) = m
source
theorem Nat.div_mul_cancel {n m : Nat} (H : n ∣ m) :
m / n * n = m
source
@[simp]
theorem Nat.mod_mod_of_dvd {c b : Nat} (a : Nat) (h : c ∣ b) :
a % b % c = a % c
source
theorem Nat.dvd_of_mul_dvd_mul_left {k m n : Nat} (kpos : 0 < k) (H : k * m ∣ k * n) :
m ∣ n
source
theorem Nat.dvd_of_mul_dvd_mul_right {k m n : Nat} (kpos : 0 < k) (H : m * k ∣ n * k) :
m ∣ n
source
theorem Nat.dvd_sub {k m n : Nat} (h₁ : k ∣ m) (h₂ : k ∣ n) :
k ∣ m - n
source
theorem Nat.dvd_sub_iff_right {m n k : Nat} (hkn : k ≤ n) (h : m ∣ n) :
m ∣ n - k ↔ m ∣ k
source
theorem Nat.dvd_sub_iff_left {m n k : Nat} (hkn : k ≤ n) (h : m ∣ k) :
m ∣ n - k ↔ m ∣ n
source
theorem Nat.mul_dvd_mul {a b c d : Nat} :
a ∣ b → c ∣ d → a * c ∣ b * d
source
theorem Nat.mul_dvd_mul_left {b c : Nat} (a : Nat) (h : b ∣ c) :
a * b ∣ a * c
source
theorem Nat.mul_dvd_mul_right {a b : Nat} (h : a ∣ b) (c : Nat) :
a * c ∣ b * c
source
@[simp]
theorem Nat.dvd_one {n : Nat} :
n ∣ 1 ↔ n = 1
source
theorem Nat.mul_div_assoc {k n : Nat} (m : Nat) (H : k ∣ n) :
m * n / k = m * (n / k)

Helper theorems for `dvd` simproc

source
theorem Nat.dvd_eq_true_of_mod_eq_zero {m n : Nat} (h : (n % m == 0) = true) :
(m ∣ n) = True
source
theorem Nat.dvd_eq_false_of_mod_ne_zero {m n : Nat} (h : (n % m != 0) = true) :
(m ∣ n) = False