HepLean Documentation

Init.Data.Nat.Div

instance Nat.instDvd :

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

@[irreducible, extern lean_nat_div]

def Nat.div (x y : Nat) :

Equations

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

Instances For

instance Nat.instDiv :

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

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

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

@[irreducible, extern lean_nat_mod]

def Nat.modCore (x y : Nat) :

Equations

x.modCore y = if 0 < y ∧ y ≤ x then (x - y).modCore y else x

Instances For

@[extern lean_nat_mod]

Nat → Nat → Nat

Equations

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

Instances For

instance Nat.instMod :

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

Equations

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

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.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

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

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

@[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.add_mul_mod_self_right (x y z : Nat) :

(x + y * z) % z = x % z

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