HepLean Documentation
Mathlib
.
Data
.
Int
.
DivMod
Search
Google site search
return to top
source
Imports
Init
Mathlib.Init
Imported by
Int
.
emod_eq_sub_self_emod
Int
.
emod_eq_add_self_emod
Basic lemmas about division and modulo for integers
#
emod
#
source
theorem
Int
.
emod_eq_sub_self_emod
{a b :
Int
}
:
a
%
b
=
(
a
-
b
)
%
b
source
theorem
Int
.
emod_eq_add_self_emod
{a b :
Int
}
:
a
%
b
=
(
a
+
b
)
%
b