Documentation

Init.Data.Nat.Div

source
@[extern lean_nat_div]
def Nat.div (a : Nat) (b : 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
@[extern lean_nat_mod]
def Nat.mod (a : Nat) (b : 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