@[simp]

theorem Nat.dvd_refl (a : Nat) : a ∣ a

@[simp]

theorem Nat.dvd_zero (a : Nat) : a ∣ 0

theorem Nat.dvd_mul_left (a b : Nat) : a ∣ b * a

theorem Nat.dvd_mul_right (a b : Nat) : a ∣ a * b

theorem Nat.dvd_trans {a b 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 b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c

theorem Nat.dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n

theorem Nat.dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n

theorem Nat.dvd_mod_iff {k m n : Nat} (h : k ∣ n) : k ∣ m % n ↔ k ∣ m

theorem Nat.le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n

theorem Nat.dvd_antisymm {m n : Nat} : m ∣ n → n ∣ m → m = n

theorem Nat.pos_of_dvd_of_pos {m 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 n : Nat} (H : m ∣ n) : n % m = 0

theorem Nat.dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n

theorem Nat.dvd_iff_mod_eq_zero {m n : Nat} : m ∣ n ↔ n % m = 0

instance Nat.decidable_dvd : DecidableRel fun (x1 x2 : Nat) => x1 ∣ x2

Equations

• x✝¹.decidable_dvd x✝ = decidable_of_decidable_of_iff ⋯

theorem Nat.emod_pos_of_not_dvd {a b : Nat} (h : ¬a ∣ b) : 0 < b % a

theorem Nat.mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m

theorem Nat.div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m

@[simp]

theorem Nat.mod_mod_of_dvd {c b : Nat} (a : Nat) (h : c ∣ b) : a % b % c = a % c

theorem Nat.dvd_of_mul_dvd_mul_left {k m n : Nat} (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n

theorem Nat.dvd_of_mul_dvd_mul_right {k m n : Nat} (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n

theorem Nat.dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n

theorem Nat.mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d

theorem Nat.mul_dvd_mul_left {b c : Nat} (a : Nat) (h : b ∣ c) : a * b ∣ a * c

theorem Nat.mul_dvd_mul_right {a 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 n : Nat} (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k)

Helper theorems for dvd simproc

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

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