mathlib documentation

core.init.data.nat.div

def nat.div (x a : ℕ) :

Equations

nat.div = nat.lt_wf.fix div.F

@[instance]

def nat.has_div :

Equations

nat.has_div = {div := nat.div}

theorem nat.div_def_aux (x y : ℕ) :

x / y = dite (0 < y ∧ y ≤ x) (λ (h : 0 < y ∧ y ≤ x), (x - y) / y + 1) (λ (h : ¬(0 < y ∧ y ≤ x)), 0)

def nat.mod (x a : ℕ) :

Equations

nat.mod = nat.lt_wf.fix mod.F

@[instance]

def nat.has_mod :

Equations

nat.has_mod = {mod := nat.mod}

theorem nat.mod_def_aux (x y : ℕ) :

x % y = dite (0 < y ∧ y ≤ x) (λ (h : 0 < y ∧ y ≤ x), (x - y) % y) (λ (h : ¬(0 < y ∧ y ≤ x)), x)