mathlib3 documentation

core / init.data.nat.div

@[protected]

def nat.div_core (y : ℕ) :

ℕ → ℕ → ℕ

Equations

y.div_core (fuel + 1) x = ite (0 < y ∧ y ≤ x) (y.div_core fuel (x - y) + 1) 0
y.div_core 0 _x = 0

@[protected]

def nat.div (x y : ℕ) :

Equations

x.div y = y.div_core x x

@[protected, instance]

def nat.has_div :

Equations

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

@[protected]

def nat.mod_core (y : ℕ) :

ℕ → ℕ → ℕ

Equations

y.mod_core (fuel + 1) x = ite (0 < y ∧ y ≤ x) (y.mod_core fuel (x - y)) x
y.mod_core 0 x = x

@[protected]

def nat.mod (x y : ℕ) :

Equations

x.mod y = y.mod_core x x

@[protected, instance]

def nat.has_mod :

Equations

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