Reducing to an interval modulo its length #
This file defines operations that reduce a number (in an archimedean
linear_ordered_add_comm_group
) to a number in a given interval, modulo the length of that
interval.
Main definitions #
to_Ico_div a hb x
(wherehb : 0 < b
): The unique integer such that this multiple ofb
, subtracted fromx
, is inIco a (a + b)
.to_Ico_mod a hb x
(wherehb : 0 < b
): Reducex
to the intervalIco a (a + b)
.to_Ioc_div a hb x
(wherehb : 0 < b
): The unique integer such that this multiple ofb
, subtracted fromx
, is inIoc a (a + b)
.to_Ioc_mod a hb x
(wherehb : 0 < b
): Reducex
to the intervalIoc a (a + b)
.
The unique integer such that this multiple of b
, subtracted from x
, is in Ico a (a + b)
.
Equations
- to_Ico_div a hb x = Exists.some _
The unique integer such that this multiple of b
, subtracted from x
, is in Ioc a (a + b)
.
Equations
- to_Ioc_div a hb x = Exists.some _
Reduce x
to the interval Ico a (a + b)
.
Equations
- to_Ico_mod a hb x = x - to_Ico_div a hb x • b
Reduce x
to the interval Ioc a (a + b)
.
Equations
- to_Ioc_mod a hb x = x - to_Ioc_div a hb x • b
Links between the Ico
and Ioc
variants applied to the same element #
mem_Ioo_mod a b x
means that x
lies in the open interval (a, a + b)
modulo b
.
Equivalently (as shown below), x
is not congruent to a
modulo b
, or to_Ico_mod a hb
agrees
with to_Ioc_mod a hb
at x
, or to_Ico_div a hb
agrees with to_Ioc_div a hb
at x
.
to_Ico_mod
as an equiv from the quotient.
Equations
- quotient_add_group.equiv_Ico_mod a hb = {to_fun := λ (x : α ⧸ add_subgroup.zmultiples b), ⟨_.lift x, _⟩, inv_fun := coe coe_to_lift, left_inv := _, right_inv := _}
to_Ioc_mod
as an equiv from the quotient.
Equations
- quotient_add_group.equiv_Ioc_mod a hb = {to_fun := λ (x : α ⧸ add_subgroup.zmultiples b), ⟨_.lift x, _⟩, inv_fun := coe coe_to_lift, left_inv := _, right_inv := _}