toNat' #
Quotient and remainder #
There are three main conventions for integer division,
referred here as the E, F, T rounding conventions.
All three pairs satisfy the identity x % y + (x / y) * y = x
unconditionally,
and satisfy x / 0 = 0
and x % 0 = x
.
E-rounding division #
This pair satisfies 0 ≤ mod x y < natAbs y
for y ≠ 0
.
T-rounding division #
This pair satisfies div x y = round_to_zero (x / y)
.
Int.div
and Int.mod
are defined in core lean.
gcd #
divisibility #
Divisibility of integers. a ∣ b
(typed as \|
) says that
there is some c
such that b = a * c
.