Documentation
Mathlib
.
Data
.
Int
.
DivMod
Search
return to top
source
Imports
Init
Mathlib.Init
Batteries.Tactic.Alias
Imported by
Int
.
mul_ediv_le_mul_ediv_assoc
Int
.
ediv_ediv_eq_ediv_mul
Int
.
fdiv_fdiv_eq_fdiv_mul
Int
.
emod_eq_sub_self_emod
Basic lemmas about division and modulo for integers
#
ediv
and
fdiv
#
source
theorem
Int
.
mul_ediv_le_mul_ediv_assoc
{
a
:
Int
}
(
ha
:
0
≤
a
)
(
b
:
Int
)
{
c
:
Int
}
(
hc
:
0
≤
c
)
:
a
*
(
b
/
c
)
≤
a
*
b
/
c
source
@[deprecated Int.ediv_ediv (since := "2025-10-06")]
theorem
Int
.
ediv_ediv_eq_ediv_mul
{
x
y
z
:
Int
}
(
hy
:
0
≤
y
)
:
x
/
y
/
z
=
x
/
(
y
*
z
)
Alias
of
Int.ediv_ediv
.
source
theorem
Int
.
fdiv_fdiv_eq_fdiv_mul
(
m
:
Int
)
{
n
k
:
Int
}
(
hn
:
0
≤
n
)
(
hk
:
0
≤
k
)
:
(
m
.
fdiv
n
)
.
fdiv
k
=
m
.
fdiv
(
n
*
k
)
emod
#
source
theorem
Int
.
emod_eq_sub_self_emod
{
a
b
:
Int
}
:
a
%
b
=
(
a
-
b
)
%
b