# 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
theorem Nat.div_rec_lemma {x : Nat} {y : Nat} :
0 < y y xx - y < x
@[extern lean_nat_div]
def Nat.div (x : Nat) (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
theorem Nat.div_eq (x : Nat) (y : Nat) :
x / y = if 0 < y y x then (x - y) / y + 1 else 0
def Nat.div.inductionOn {motive : NatNatSort u} (x : Nat) (y : Nat) (ind : (x y : Nat) → 0 < y y xmotive (x - y) ymotive x y) (base : (x y : Nat) → ¬(0 < y y x)motive x y) :
motive x y
Equations
Instances For
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
@[extern lean_nat_mod]
def Nat.modCore (x : Nat) (y : Nat) :
Equations
• x.modCore y = if 0 < y y x then (x - y).modCore y else x
Instances For
@[extern lean_nat_mod]
def Nat.mod :
Equations
• x✝.mod x = match x✝, x with | 0, x => 0 | x@h:n.succ, y => x.modCore y
Instances For
instance Nat.instMod :
Equations
theorem Nat.modCore_eq_mod (x : Nat) (y : Nat) :
x.modCore y = x % y
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 : NatNatSort u} (x : Nat) (y : Nat) (ind : (x y : Nat) → 0 < y y xmotive (x - y) ymotive x y) (base : (x y : Nat) → ¬(0 < y y x)motive x y) :
motive x y
Equations
Instances For
@[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 > 0x % 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
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
@[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).succ
@[simp]
theorem Nat.add_div_left (x : Nat) {z : Nat} (H : 0 < z) :
(z + x) / z = (x / z).succ
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.succ * 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.succ) / n = p - (x / n).succ
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 * nm / 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