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

@[irreducible, extern lean_nat_div]

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

Equations

• x.div y = if 0 < y ∧ y ≤ x then (x - y).div y + 1 else 0

instance Nat.instDiv : Div Nat

Equations

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

theorem Nat.div_eq (x : Nat) (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 : Nat) (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

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 : Nat) (k : Nat) : n / k ≤ n

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

@[irreducible, extern lean_nat_mod]

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

Equations

• 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

Equations

• x✝.mod x = match x✝, x with | 0, x => 0 | n@h:n_1.succ, m => if m ≤ n then n.modCore m else n

instance Nat.instMod : Mod Nat

Equations

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

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

theorem Nat.mod_eq (x : Nat) (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 : Nat) (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

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 : Nat} {b : Nat} (h : a < b) : a % b = a

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

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

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

@[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 : Nat) (n : Nat) : n * (m / n) + m % n = m

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

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

theorem Nat.mod_def (m : Nat) (k : Nat) : m % k = m - k * (m / 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 : Nat} {x : Nat} {y : Nat} (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y

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

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

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

@[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 : Nat) (z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem Nat.div_eq_of_lt {a : Nat} {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 : Nat} {n : Nat} {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 : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = k * n) : m / n = k

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

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

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

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