Documentation

Init.Data.Nat.Div

source
theorem Nat.div_rec_lemma {x : Nat} {y : Nat} :
0 < y ∧ y ≤ x → x - y < x
source
@[extern lean_nat_div]
def Nat.div (x : Nat) (y : Nat) :
Nat
Equations
source
instance Nat.instDivNat :
Div Nat
Equations
source
theorem Nat.div_eq (x : Nat) (y : Nat) :
x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0
source
theorem 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
source
theorem Nat.div_le_self (n : Nat) (k : Nat) :
n / k ≤ n
source
theorem Nat.div_lt_self {n : Nat} {k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) :
n / k < n
source
@[extern lean_nat_mod]
def Nat.mod (x : Nat) (y : Nat) :
Nat
Equations
source
instance Nat.instModNat :
Mod Nat
Equations
source
theorem Nat.mod_eq (x : Nat) (y : Nat) :
x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x
source
theorem 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
source
theorem Nat.mod_zero (a : Nat) :
a % 0 = a
source
theorem Nat.mod_eq_of_lt {a : Nat} {b : Nat} (h : a < b) :
a % b = a
source
theorem Nat.mod_eq_sub_mod {a : Nat} {b : Nat} (h : a ≥ b) :
a % b = (a - b) % b
source
theorem Nat.mod_lt (x : Nat) {y : Nat} :
y > 0 → x % y < y
source
theorem Nat.mod_le (x : Nat) (y : Nat) :
x % y ≤ x
source
@[simp]
theorem Nat.zero_mod (b : Nat) :
0 % b = 0
source
@[simp]
theorem Nat.mod_self (n : Nat) :
n % n = 0
source
theorem Nat.mod_one (x : Nat) :
x % 1 = 0
source
theorem Nat.div_add_mod (m : Nat) (n : Nat) :
n * (m / n) + m % n = m