Documentation

Init.Data.Nat.Div.Basic

instance Nat.instDvd :

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

Equations

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

Instances For

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) :

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

Instances For

@[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

Instances For

@[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