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_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x

theorem Nat.div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y ≤ x) (hfuel : x < fuel + 1) : x - y < fuel

@[irreducible, extern lean_nat_div]

def Nat.div (x y : Nat) : Nat

Division of natural numbers, discarding the remainder. Division by 0 returns 0. Usually accessed via the / operator.

This operation is sometimes called “floor division.”

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

Examples:

• 21 / 3 = 7
• 21 / 5 = 4
• 0 / 22 = 0
• 5 / 0 = 0

Equations

• x.div y = if hy : 0 < y then Nat.div.go y hy (x + 1) x ⋯ else 0

def Nat.div.go (y : Nat) (hy : 0 < y) (fuel x : Nat) (hfuel : x < fuel) : Nat

Equations

• Nat.div.go y hy 0 x hfuel_2 = ⋯.elim
• Nat.div.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.div.go y hy fuel_2 (x - y) ⋯ + 1 else 0

instance Nat.instDiv : Div Nat

Equations

• Nat.instDiv = { div := Nat.div }

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

@[irreducible, extern lean_nat_mod]

noncomputable def Nat.modCore (x y : Nat) : Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

This is the core implementation of Nat.mod. It computes the correct result for any two closed natural numbers, but it does not have some convenient definitional reductions when the Nats contain free variables. The wrapper Nat.mod handles those cases specially and then calls Nat.modCore.

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

Equations

• x.modCore y = if hy : 0 < y then Nat.modCore.go y hy (x + 1) x ⋯ else x

noncomputable def Nat.modCore.go (y : Nat) (hy : 0 < y) (fuel x : Nat) (hfuel : x < fuel) : Nat

Equations

• Nat.modCore.go y hy 0 x hfuel_2 = ⋯.elim
• Nat.modCore.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.modCore.go y hy fuel_2 (x - y) ⋯ else x

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

@[extern lean_nat_mod]

def Nat.mod : Nat → Nat → Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

Nat.mod is a wrapper around Nat.modCore that special-cases two situations, giving better definitional reductions:

• Nat.mod 0 m should reduce to m, for all terms m : Nat.
• Nat.mod n (m + n + 1) should reduce to n for concrete Nat literals n.

These reductions help Fin n literals work well, because the OfNat instance for Fin uses Nat.mod. In particular, (0 : Fin (n + 1)).val should reduce definitionally to 0. Nat.modCore can handle all numbers, but its definitional reductions are not as convenient.

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

Examples:

• 7 % 2 = 1
• 9 % 3 = 0
• 5 % 7 = 5
• 5 % 0 = 5
• show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl
• show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl

Equations

• Nat.mod 0 x✝ = 0
• n.succ.mod x✝ = if x✝ ≤ n.succ then n.succ.modCore x✝ else n.succ

instance Nat.instMod : Mod Nat

Equations

• Nat.instMod = { mod := Nat.mod }

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

theorem Nat.mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y

@[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 (x n p : Nat) (h₁ : n * p ≤ x) : (x - n * p) / n = x / n - p

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

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