mathlib documentation

core.init.data.nat.div

def nat.div  :

Equations
@[instance]

Equations
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  :

Equations
@[instance]

Equations
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)