# mathlib3documentation

algebra.order.to_interval_mod

# Reducing to an interval modulo its length #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 hp a b (where hp : 0 < p): The unique integer such that this multiple of p, subtracted from b, is in Ico a (a + p).
• to_Ico_mod hp a b (where hp : 0 < p): Reduce b to the interval Ico a (a + p).
• to_Ioc_div hp a b (where hp : 0 < p): The unique integer such that this multiple of p, subtracted from b, is in Ioc a (a + p).
• to_Ioc_mod hp a b (where hp : 0 < p): Reduce b to the interval Ioc a (a + p).
noncomputable def to_Ico_div {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :

The unique integer such that this multiple of p, subtracted from b, is in Ico a (a + p).

Equations
• a b =
theorem sub_to_Ico_div_zsmul_mem_Ico {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - a b p (a + p)
theorem to_Ico_div_eq_of_sub_zsmul_mem_Ico {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} {n : } (h : b - n p (a + p)) :
a b = n
noncomputable def to_Ioc_div {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :

The unique integer such that this multiple of p, subtracted from b, is in Ioc a (a + p).

Equations
• a b =
theorem sub_to_Ioc_div_zsmul_mem_Ioc {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - a b p (a + p)
theorem to_Ioc_div_eq_of_sub_zsmul_mem_Ioc {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} {n : } (h : b - n p (a + p)) :
a b = n
noncomputable def to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
α

Reduce b to the interval Ico a (a + p).

Equations
noncomputable def to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
α

Reduce b to the interval Ioc a (a + p).

Equations
theorem to_Ico_mod_mem_Ico {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b (a + p)
theorem to_Ico_mod_mem_Ico' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (b : α) :
0 b p
theorem to_Ioc_mod_mem_Ioc {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b (a + p)
theorem left_le_to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a a b
theorem left_lt_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a < a b
theorem to_Ico_mod_lt_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b < a + p
theorem to_Ioc_mod_le_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b a + p
@[simp]
theorem self_sub_to_Ico_div_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - a b p = a b
@[simp]
theorem self_sub_to_Ioc_div_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - a b p = a b
@[simp]
theorem to_Ico_div_zsmul_sub_self {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b p - b = - a b
@[simp]
theorem to_Ioc_div_zsmul_sub_self {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b p - b = - a b
@[simp]
theorem to_Ico_mod_sub_self {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b - b = - a b p
@[simp]
theorem to_Ioc_mod_sub_self {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b - b = - a b p
@[simp]
theorem self_sub_to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - a b = a b p
@[simp]
theorem self_sub_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - a b = a b p
@[simp]
theorem to_Ico_mod_add_to_Ico_div_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b + a b p = b
@[simp]
theorem to_Ioc_mod_add_to_Ioc_div_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b + a b p = b
@[simp]
theorem to_Ico_div_zsmul_sub_to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b p + a b = b
@[simp]
theorem to_Ioc_div_zsmul_sub_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b p + a b = b
theorem to_Ico_mod_eq_iff {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
a b = c c (a + p) (z : ), b = c + z p
theorem to_Ioc_mod_eq_iff {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
a b = c c (a + p) (z : ), b = c + z p
@[simp]
theorem to_Ico_div_apply_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a a = 0
@[simp]
theorem to_Ioc_div_apply_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a a = -1
@[simp]
theorem to_Ico_mod_apply_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a a = a
@[simp]
theorem to_Ioc_mod_apply_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a a = a + p
theorem to_Ico_div_apply_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a (a + p) = 1
theorem to_Ioc_div_apply_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a (a + p) = 0
theorem to_Ico_mod_apply_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a (a + p) = a
theorem to_Ioc_mod_apply_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
a (a + p) = a + p
@[simp]
theorem to_Ico_div_add_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b + m p) = a b + m
@[simp]
theorem to_Ico_div_add_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a + m p) b = a b - m
@[simp]
theorem to_Ioc_div_add_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b + m p) = a b + m
@[simp]
theorem to_Ioc_div_add_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a + m p) b = a b - m
@[simp]
theorem to_Ico_div_zsmul_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (m p + b) = m + a b

Note we omit to_Ico_div_zsmul_add' as -m + to_Ico_div hp a b is not very convenient.

@[simp]
theorem to_Ioc_div_zsmul_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (m p + b) = m + a b

Note we omit to_Ioc_div_zsmul_add' as -m + to_Ioc_div hp a b is not very convenient.

@[simp]
theorem to_Ico_div_sub_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b - m p) = a b - m
@[simp]
theorem to_Ico_div_sub_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a - m p) b = a b + m
@[simp]
theorem to_Ioc_div_sub_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b - m p) = a b - m
@[simp]
theorem to_Ioc_div_sub_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a - m p) b = a b + m
@[simp]
theorem to_Ico_div_add_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b + p) = a b + 1
@[simp]
theorem to_Ico_div_add_right' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a + p) b = a b - 1
@[simp]
theorem to_Ioc_div_add_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b + p) = a b + 1
@[simp]
theorem to_Ioc_div_add_right' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a + p) b = a b - 1
@[simp]
theorem to_Ico_div_add_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (p + b) = a b + 1
@[simp]
theorem to_Ico_div_add_left' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(p + a) b = a b - 1
@[simp]
theorem to_Ioc_div_add_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (p + b) = a b + 1
@[simp]
theorem to_Ioc_div_add_left' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(p + a) b = a b - 1
@[simp]
theorem to_Ico_div_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b - p) = a b - 1
@[simp]
theorem to_Ico_div_sub' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a - p) b = a b + 1
@[simp]
theorem to_Ioc_div_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b - p) = a b - 1
@[simp]
theorem to_Ioc_div_sub' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a - p) b = a b + 1
theorem to_Ico_div_sub_eq_to_Ico_div_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
a (b - c) = (a + c) b
theorem to_Ioc_div_sub_eq_to_Ioc_div_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
a (b - c) = (a + c) b
theorem to_Ico_div_sub_eq_to_Ico_div_add' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
(a - c) b = a (b + c)
theorem to_Ioc_div_sub_eq_to_Ioc_div_add' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
(a - c) b = a (b + c)
theorem to_Ico_div_neg {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (-b) = -(to_Ioc_div hp (-a) b + 1)
theorem to_Ico_div_neg' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(-a) b = -(to_Ioc_div hp a (-b) + 1)
theorem to_Ioc_div_neg {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (-b) = -(to_Ico_div hp (-a) b + 1)
theorem to_Ioc_div_neg' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(-a) b = -(to_Ico_div hp a (-b) + 1)
@[simp]
theorem to_Ico_mod_add_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b + m p) = a b
@[simp]
theorem to_Ico_mod_add_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a + m p) b = a b + m p
@[simp]
theorem to_Ioc_mod_add_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b + m p) = a b
@[simp]
theorem to_Ioc_mod_add_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a + m p) b = a b + m p
@[simp]
theorem to_Ico_mod_zsmul_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (m p + b) = a b
@[simp]
theorem to_Ico_mod_zsmul_add' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(m p + a) b = m p + a b
@[simp]
theorem to_Ioc_mod_zsmul_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (m p + b) = a b
@[simp]
theorem to_Ioc_mod_zsmul_add' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(m p + a) b = m p + a b
@[simp]
theorem to_Ico_mod_sub_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b - m p) = a b
@[simp]
theorem to_Ico_mod_sub_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a - m p) b = a b - m p
@[simp]
theorem to_Ioc_mod_sub_zsmul {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
a (b - m p) = a b
@[simp]
theorem to_Ioc_mod_sub_zsmul' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
(a - m p) b = a b - m p
@[simp]
theorem to_Ico_mod_add_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b + p) = a b
@[simp]
theorem to_Ico_mod_add_right' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a + p) b = a b + p
@[simp]
theorem to_Ioc_mod_add_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b + p) = a b
@[simp]
theorem to_Ioc_mod_add_right' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a + p) b = a b + p
@[simp]
theorem to_Ico_mod_add_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (p + b) = a b
@[simp]
theorem to_Ico_mod_add_left' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(p + a) b = p + a b
@[simp]
theorem to_Ioc_mod_add_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (p + b) = a b
@[simp]
theorem to_Ioc_mod_add_left' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(p + a) b = p + a b
@[simp]
theorem to_Ico_mod_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b - p) = a b
@[simp]
theorem to_Ico_mod_sub' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a - p) b = a b - p
@[simp]
theorem to_Ioc_mod_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (b - p) = a b
@[simp]
theorem to_Ioc_mod_sub' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(a - p) b = a b - p
theorem to_Ico_mod_sub_eq_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
a (b - c) = (a + c) b - c
theorem to_Ioc_mod_sub_eq_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
a (b - c) = (a + c) b - c
theorem to_Ico_mod_add_right_eq_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
a (b + c) = (a - c) b + c
theorem to_Ioc_mod_add_right_eq_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
a (b + c) = (a - c) b + c
theorem to_Ico_mod_neg {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (-b) = p - (-a) b
theorem to_Ico_mod_neg' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(-a) b = p - a (-b)
theorem to_Ioc_mod_neg {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a (-b) = p - (-a) b
theorem to_Ioc_mod_neg' {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
(-a) b = p - a (-b)
theorem to_Ico_mod_eq_to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
a b = a c (n : ), c - b = n p
theorem to_Ioc_mod_eq_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
a b = a c (n : ), c - b = n p
theorem add_comm_group.modeq_iff_to_Ico_mod_eq_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] a b = a
theorem add_comm_group.modeq_iff_to_Ioc_mod_eq_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] a b = a + p
theorem add_comm_group.modeq.to_Ico_mod_eq_left {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] a b = a

Alias of the forward direction of add_comm_group.modeq_iff_to_Ico_mod_eq_left.

theorem add_comm_group.modeq.to_Ico_mod_eq_right {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] a b = a + p

Alias of the forward direction of add_comm_group.modeq_iff_to_Ioc_mod_eq_right.

theorem add_comm_group.tfae_modeq {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
[a b [PMOD p], (z : ), b - z p (a + p), a b a b, a b + p = a b].tfae
theorem add_comm_group.modeq_iff_not_forall_mem_Ioo_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] (z : ), b - z p (a + p)
theorem add_comm_group.modeq_iff_to_Ico_mod_ne_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] a b a b
theorem add_comm_group.modeq_iff_to_Ico_mod_add_period_eq_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] a b + p = a b
theorem add_comm_group.not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
¬a b [PMOD p] a b = a b
theorem add_comm_group.not_modeq_iff_to_Ico_div_eq_to_Ioc_div {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
¬a b [PMOD p] a b = a b
theorem add_comm_group.modeq_iff_to_Ico_div_eq_to_Ioc_div_add_one {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] a b = a b + 1
@[simp]
theorem to_Ico_mod_inj {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
c a = c b a b [PMOD p]

If a and b fall within the same cycle WRT c, then they are congruent modulo p.

theorem add_comm_group.modeq.to_Ico_mod_eq_to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
a b [PMOD p] c a = c b

Alias of the reverse direction of to_Ico_mod_inj.

theorem Ico_eq_locus_Ioc_eq_Union_Ioo {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a : α} :
{b : α | a b = a b} = (z : ), set.Ioo (a + z p) (a + p + z p)
theorem to_Ioc_div_wcovby_to_Ico_div {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b ⩿ a b
theorem to_Ico_mod_le_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b a b
theorem to_Ioc_mod_le_to_Ico_mod_add {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b a b + p
theorem to_Ico_mod_eq_self {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b = b b (a + p)
theorem to_Ioc_mod_eq_self {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b = b b (a + p)
@[simp]
theorem to_Ico_mod_to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
a₁ (to_Ico_mod hp a₂ b) = a₁ b
@[simp]
theorem to_Ico_mod_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
a₁ (to_Ioc_mod hp a₂ b) = a₁ b
@[simp]
theorem to_Ioc_mod_to_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
a₁ (to_Ioc_mod hp a₂ b) = a₁ b
@[simp]
theorem to_Ioc_mod_to_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
a₁ (to_Ico_mod hp a₂ b) = a₁ b
theorem to_Ico_mod_periodic {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
theorem to_Ioc_mod_periodic {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
theorem to_Ico_mod_zero_sub_comm {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
0 (a - b) = p - 0 (b - a)
theorem to_Ioc_mod_zero_sub_comm {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
0 (a - b) = p - 0 (b - a)
theorem to_Ico_div_eq_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b = 0 (b - a)
theorem to_Ioc_div_eq_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b = 0 (b - a)
theorem to_Ico_mod_eq_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b = 0 (b - a) + a
theorem to_Ioc_mod_eq_sub {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a b = 0 (b - a) + a
theorem to_Ico_mod_add_to_Ioc_mod_zero {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
0 (a - b) + 0 (b - a) = p
theorem to_Ioc_mod_add_to_Ico_mod_zero {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
0 (a - b) + 0 (b - a) = p
@[simp]
theorem quotient_add_group.equiv_Ico_mod_symm_apply {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) (ᾰ : (set.Ico a (a + p))) :
.symm) =
noncomputable def quotient_add_group.equiv_Ico_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
(set.Ico a (a + p))

to_Ico_mod as an equiv from the quotient.

Equations
@[simp]
theorem quotient_add_group.equiv_Ico_mod_coe {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
= a b, _⟩
@[simp]
theorem quotient_add_group.equiv_Ico_mod_zero {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
= a 0, _⟩
noncomputable def quotient_add_group.equiv_Ioc_mod {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
(set.Ioc a (a + p))

to_Ioc_mod as an equiv from the quotient.

Equations
@[simp]
theorem quotient_add_group.equiv_Ioc_mod_symm_apply {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) (ᾰ : (set.Ioc a (a + p))) :
.symm) =
@[simp]
theorem quotient_add_group.equiv_Ioc_mod_coe {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
= a b, _⟩
@[simp]
theorem quotient_add_group.equiv_Ioc_mod_zero {α : Type u_1} [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
= a 0, _⟩

### The circular order structure on α ⧸ add_subgroup.zmultiples p#

@[protected, instance]
def quotient_add_group.has_quotient.quotient.has_btw {α : Type u_1} [hα : archimedean α] {p : α} [hp' : fact (0 < p)] :
Equations
theorem quotient_add_group.btw_coe_iff' {α : Type u_1} [hα : archimedean α] {p : α} [hp' : fact (0 < p)] {x₁ x₂ x₃ : α} :
x₂ x₃ 0 (x₂ - x₁) 0 (x₃ - x₁)
theorem quotient_add_group.btw_coe_iff {α : Type u_1} [hα : archimedean α] {p : α} [hp' : fact (0 < p)] {x₁ x₂ x₃ : α} :
x₂ x₃ x₁ x₂ x₁ x₃
@[protected, instance]
def quotient_add_group.circular_preorder {α : Type u_1} [hα : archimedean α] {p : α} [hp' : fact (0 < p)] :
Equations
@[protected, instance]
def quotient_add_group.circular_order {α : Type u_1} [hα : archimedean α] {p : α} [hp' : fact (0 < p)] :
Equations

### Connections to int.floor and int.fract#

theorem to_Ico_div_eq_floor {α : Type u_1} [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
a b = (b - a) / p
theorem to_Ioc_div_eq_neg_floor {α : Type u_1} [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
a b = -(a + p - b) / p
theorem to_Ico_div_zero_one {α : Type u_1} [floor_ring α] (b : α) :
0 b = b
theorem to_Ico_mod_eq_add_fract_mul {α : Type u_1} [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
a b = a + int.fract ((b - a) / p) * p
theorem to_Ico_mod_eq_fract_mul {α : Type u_1} [floor_ring α] {p : α} (hp : 0 < p) (b : α) :
0 b = int.fract (b / p) * p
theorem to_Ioc_mod_eq_sub_fract_mul {α : Type u_1} [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
a b = a + p - int.fract ((a + p - b) / p) * p
theorem to_Ico_mod_zero_one {α : Type u_1} [floor_ring α] (b : α) :
0 b =

### Lemmas about unions of translates of intervals #

theorem Union_Ioc_add_zsmul {α : Type u_1} [archimedean α] {p : α} (hp : 0 < p) (a : α) :
( (n : ), set.Ioc (a + n p) (a + (n + 1) p)) = set.univ
theorem Union_Ico_add_zsmul {α : Type u_1} [archimedean α] {p : α} (hp : 0 < p) (a : α) :
( (n : ), set.Ico (a + n p) (a + (n + 1) p)) = set.univ
theorem Union_Icc_add_zsmul {α : Type u_1} [archimedean α] {p : α} (hp : 0 < p) (a : α) :
( (n : ), set.Icc (a + n p) (a + (n + 1) p)) = set.univ
theorem Union_Ioc_zsmul {α : Type u_1} [archimedean α] {p : α} (hp : 0 < p) :
( (n : ), set.Ioc (n p) ((n + 1) p)) = set.univ
theorem Union_Ico_zsmul {α : Type u_1} [archimedean α] {p : α} (hp : 0 < p) :
( (n : ), set.Ico (n p) ((n + 1) p)) = set.univ
theorem Union_Icc_zsmul {α : Type u_1} [archimedean α] {p : α} (hp : 0 < p) :
( (n : ), set.Icc (n p) ((n + 1) p)) = set.univ
theorem Union_Ioc_add_int_cast {α : Type u_1} [archimedean α] (a : α) :
( (n : ), set.Ioc (a + n) (a + n + 1)) = set.univ
theorem Union_Ico_add_int_cast {α : Type u_1} [archimedean α] (a : α) :
( (n : ), set.Ico (a + n) (a + n + 1)) = set.univ
theorem Union_Icc_add_int_cast {α : Type u_1} [archimedean α] (a : α) :
( (n : ), set.Icc (a + n) (a + n + 1)) = set.univ
theorem Union_Ioc_int_cast (α : Type u_1) [archimedean α] :
( (n : ), (n + 1)) = set.univ
theorem Union_Ico_int_cast (α : Type u_1) [archimedean α] :
( (n : ), (n + 1)) = set.univ
theorem Union_Icc_int_cast (α : Type u_1) [archimedean α] :
( (n : ), (n + 1)) = set.univ