mathlib documentation

core / init.data.nat.div

def nat.div (x : ) :
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 (x : ) :
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)