instance Nat.instDvdNat : Dvd Nat

Divisibility of natural numbers. a ∣ b (typed as \|) says that there is some c such that b = a * c.

Equations

• Nat.instDvdNat = { dvd := fun (a b : Nat) => ∃ (c : Nat), b = a * c }

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 ∣ n → m ≤ n

theorem Nat.dvd_antisymm {m : Nat} {n : Nat} : m ∣ n → n ∣ m → m = 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 (x x_1 : Nat) => x ∣ x_1

Equations

• Nat.decidable_dvd x✝ x = decidable_of_decidable_of_iff ⋯

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