mathlib documentation

core / init.data.nat.div

@[protected]
def nat.div_core (y : ) :
Equations
@[protected]
def nat.div (x y : ) :
Equations
@[protected, instance]
Equations
@[protected]
def nat.mod_core (y : ) :
Equations
@[protected]
def nat.mod (x y : ) :
Equations
@[protected, instance]
Equations