instance Nat.instDvd : Dvd Nat

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

Equations

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

theorem Nat.div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0

@[irreducible]

def Nat.div.inductionOn {motive : Nat → Nat → Sort u} (x y : Nat) (ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) (base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y) : motive x y

An induction principle customized for reasoning about the recursion pattern of natural number division by iterated subtraction.

Equations

• Nat.div.inductionOn x y ind base = if h : 0 < y ∧ y ≤ x then ind x y h (Nat.div.inductionOn (x - y) y ind base) else base x y h

theorem Nat.div_le_self (n k : Nat) : n / k ≤ n

theorem Nat.div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n

@[extern lean_nat_div_exact]

def Nat.divExact (x y : Nat) (h : y ∣ x) : Nat

Division of two divisible natural numbers. Division by 0 returns 0.

This operation uses an optimized implementation, specialized for two divisible natural numbers.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

• Nat.divExact 21 3 (by decide) = 7
• Nat.divExact 0 22 (by decide) = 0
• Nat.divExact 0 0 (by decide) = 0

Equations

• x.divExact y h = x / y

@[simp]

theorem Nat.divExact_eq_div {x y : Nat} (h : y ∣ x) : x.divExact y h = x / y

theorem Nat.modCore_eq (x y : Nat) : x.modCore y = if 0 < y ∧ y ≤ x then (x - y).modCore y else x

theorem Nat.modCore_eq_mod (n m : Nat) : n.modCore m = n % m

theorem Nat.mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x

def Nat.mod.inductionOn {motive : Nat → Nat → Sort u} (x y : Nat) (ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) (base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y) : motive x y

An induction principle customized for reasoning about the recursion pattern of Nat.mod.

Equations

• Nat.mod.inductionOn x y ind base = Nat.div.inductionOn x y ind base

@[simp]

theorem Nat.mod_zero (a : Nat) : a % 0 = a

theorem Nat.mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a

@[simp]

theorem Nat.one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1

@[simp]

theorem Nat.zero_eq_one_mod_iff {n : Nat} : 0 = 1 % n ↔ n = 1

theorem Nat.mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b

@[simp]

theorem Nat.sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a

theorem Nat.mod_le (x y : Nat) : x % y ≤ x

theorem Nat.mod_lt_of_lt {a b c : Nat} (h : a < c) : a % b < c

@[simp]

theorem Nat.zero_mod (b : Nat) : 0 % b = 0

@[simp]

theorem Nat.mod_self (n : Nat) : n % n = 0

theorem Nat.mod_one (x : Nat) : x % 1 = 0

@[irreducible]

theorem Nat.div_add_mod (m n : Nat) : n * (m / n) + m % n = m

theorem Nat.div_eq_sub_div {b a : Nat} (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1

theorem Nat.mod_add_div (m k : Nat) : m % k + k * (m / k) = m

theorem Nat.mod_def (m k : Nat) : m % k = m - k * (m / k)

theorem Nat.mod_eq_sub_mul_div {x k : Nat} : x % k = x - k * (x / k)

theorem Nat.mod_eq_sub_div_mul {x k : Nat} : x % k = x - x / k * k

@[simp]

theorem Nat.div_one (n : Nat) : n / 1 = n

@[simp]

theorem Nat.div_zero (n : Nat) : n / 0 = 0

@[simp]

theorem Nat.zero_div (b : Nat) : 0 / b = 0

theorem Nat.le_div_iff_mul_le {k x y : Nat} (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y

theorem Nat.div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k)

theorem Nat.div_mul_le_self (m n : Nat) : m / n * n ≤ m

theorem Nat.div_lt_iff_lt_mul {k x y : Nat} (Hk : 0 < k) : x / k < y ↔ x < y * k

theorem Nat.pos_of_div_pos {a b : Nat} (h : 0 < a / b) : 0 < a

@[simp]

theorem Nat.add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = x / z + 1

@[simp]

theorem Nat.add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = x / z + 1

theorem Nat.add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z

theorem Nat.add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y

@[simp]

theorem Nat.add_mod_right (x z : Nat) : (x + z) % z = x % z

@[simp]

theorem Nat.add_mod_left (x z : Nat) : (x + z) % x = z % x

@[simp]

theorem Nat.add_mul_mod_self_left (x y z : Nat) : (x + y * z) % y = x % y

@[simp]

theorem Nat.mul_add_mod_self_left (a b c : Nat) : (a * b + c) % a = c % a

@[simp]

theorem Nat.add_mul_mod_self_right (x y z : Nat) : (x + y * z) % z = x % z

@[simp]

theorem Nat.mul_add_mod_self_right (a b c : Nat) : (a * b + c) % b = c % b

@[simp]

theorem Nat.mul_mod_right (m n : Nat) : m * n % m = 0

@[simp]

theorem Nat.mul_mod_left (m n : Nat) : m * n % n = 0

theorem Nat.div_eq_of_lt_le {k n m : Nat} (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k

theorem Nat.sub_mul_div_of_le (x n p : Nat) (h₁ : n * p ≤ x) : (x - n * p) / n = x / n - p

See also sub_mul_div for a strictly more general version.

theorem Nat.mul_sub_div (x n p : Nat) (h₁ : x < n * p) : (n * p - (x + 1)) / n = p - (x / n + 1)

theorem Nat.mul_mod_mul_left (z x y : Nat) : z * x % (z * y) = z * (x % y)

theorem Nat.div_eq_of_lt {a b : Nat} (h₀ : a < b) : a / b = 0

theorem Nat.mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

theorem Nat.mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m

theorem Nat.div_le_of_le_mul {m n k : Nat} : m ≤ k * n → m / k ≤ n

@[simp]

theorem Nat.mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n

@[simp]

theorem Nat.mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

@[simp]

theorem Nat.div_self {n : Nat} (H : 0 < n) : n / n = 1

theorem Nat.div_eq_of_eq_mul_left {n m k : Nat} (H1 : 0 < n) (H2 : m = k * n) : m / n = k

theorem Nat.div_eq_of_eq_mul_right {n m k : Nat} (H1 : 0 < n) (H2 : m = n * k) : m / n = k

theorem Nat.mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) : m * n / (m * k) = n / k

theorem Nat.mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) : n * m / (k * m) = n / k

theorem Nat.mul_div_le (m n : Nat) : n * (m / n) ≤ m