Documentation
EvmEquivalence
.
Utils
.
IntUtils
Search
return to top
source
Imports
Aesop
Init
Mathlib.Order.Lattice
Imported by
Int
.
mod_cast
source
theorem
Int
.
mod_cast
{
n
m
:
ℤ
}
(
le0n
:
0
≤
n
)
(
le0m
:
0
≤
m
)
:
n
%
m
=
↑(
n
.
toNat
%
m
.
toNat
)