# Reducing to an interval modulo its length #

This file defines operations that reduce a number (in an Archimedean LinearOrderedAddCommGroup) to a number in a given interval, modulo the length of that interval.

## Main definitions #

• toIcoDiv 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).
• toIcoMod hp a b (where hp : 0 < p): Reduce b to the interval Ico a (a + p).
• toIocDiv 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).
• toIocMod hp a b (where hp : 0 < p): Reduce b to the interval Ioc a (a + p).
def toIcoDiv {α : Type u_1} [hα : ] {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
Instances For
theorem sub_toIcoDiv_zsmul_mem_Ico {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
b - toIcoDiv hp a b p Set.Ico a (a + p)
theorem toIcoDiv_eq_of_sub_zsmul_mem_Ico {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {n : } (h : b - n p Set.Ico a (a + p)) :
toIcoDiv hp a b = n
def toIocDiv {α : Type u_1} [hα : ] {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
Instances For
theorem sub_toIocDiv_zsmul_mem_Ioc {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
b - toIocDiv hp a b p Set.Ioc a (a + p)
theorem toIocDiv_eq_of_sub_zsmul_mem_Ioc {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {n : } (h : b - n p Set.Ioc a (a + p)) :
toIocDiv hp a b = n
def toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
α

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

Equations
Instances For
def toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
α

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

Equations
Instances For
theorem toIcoMod_mem_Ico {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a b Set.Ico a (a + p)
theorem toIcoMod_mem_Ico' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (b : α) :
toIcoMod hp 0 b Set.Ico 0 p
theorem toIocMod_mem_Ioc {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a b Set.Ioc a (a + p)
theorem left_le_toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
a toIcoMod hp a b
theorem left_lt_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
a < toIocMod hp a b
theorem toIcoMod_lt_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a b < a + p
theorem toIocMod_le_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a b a + p
@[simp]
theorem self_sub_toIcoDiv_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
b - toIcoDiv hp a b p = toIcoMod hp a b
@[simp]
theorem self_sub_toIocDiv_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
b - toIocDiv hp a b p = toIocMod hp a b
@[simp]
theorem toIcoDiv_zsmul_sub_self {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a b p - b = -toIcoMod hp a b
@[simp]
theorem toIocDiv_zsmul_sub_self {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a b p - b = -toIocMod hp a b
@[simp]
theorem toIcoMod_sub_self {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a b - b = -toIcoDiv hp a b p
@[simp]
theorem toIocMod_sub_self {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a b - b = -toIocDiv hp a b p
@[simp]
theorem self_sub_toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
b - toIcoMod hp a b = toIcoDiv hp a b p
@[simp]
theorem self_sub_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
b - toIocMod hp a b = toIocDiv hp a b p
@[simp]
theorem toIcoMod_add_toIcoDiv_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a b + toIcoDiv hp a b p = b
@[simp]
theorem toIocMod_add_toIocDiv_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a b + toIocDiv hp a b p = b
@[simp]
theorem toIcoDiv_zsmul_sub_toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a b p + toIcoMod hp a b = b
@[simp]
theorem toIocDiv_zsmul_sub_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a b p + toIocMod hp a b = b
theorem toIcoMod_eq_iff {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {c : α} :
toIcoMod hp a b = c c Set.Ico a (a + p) ∃ (z : ), b = c + z p
theorem toIocMod_eq_iff {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {c : α} :
toIocMod hp a b = c c Set.Ioc a (a + p) ∃ (z : ), b = c + z p
@[simp]
theorem toIcoDiv_apply_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIcoDiv hp a a = 0
@[simp]
theorem toIocDiv_apply_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIocDiv hp a a = -1
@[simp]
theorem toIcoMod_apply_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIcoMod hp a a = a
@[simp]
theorem toIocMod_apply_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIocMod hp a a = a + p
theorem toIcoDiv_apply_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIcoDiv hp a (a + p) = 1
theorem toIocDiv_apply_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIocDiv hp a (a + p) = 0
theorem toIcoMod_apply_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIcoMod hp a (a + p) = a
theorem toIocMod_apply_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
toIocMod hp a (a + p) = a + p
@[simp]
theorem toIcoDiv_add_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoDiv hp a (b + m p) = toIcoDiv hp a b + m
@[simp]
theorem toIcoDiv_add_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoDiv hp (a + m p) b = toIcoDiv hp a b - m
@[simp]
theorem toIocDiv_add_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocDiv hp a (b + m p) = toIocDiv hp a b + m
@[simp]
theorem toIocDiv_add_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocDiv hp (a + m p) b = toIocDiv hp a b - m
@[simp]
theorem toIcoDiv_zsmul_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoDiv hp a (m p + b) = m + toIcoDiv hp a b

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

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

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

@[simp]
theorem toIcoDiv_sub_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoDiv hp a (b - m p) = toIcoDiv hp a b - m
@[simp]
theorem toIcoDiv_sub_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoDiv hp (a - m p) b = toIcoDiv hp a b + m
@[simp]
theorem toIocDiv_sub_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocDiv hp a (b - m p) = toIocDiv hp a b - m
@[simp]
theorem toIocDiv_sub_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocDiv hp (a - m p) b = toIocDiv hp a b + m
@[simp]
theorem toIcoDiv_add_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1
@[simp]
theorem toIcoDiv_add_right' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1
@[simp]
theorem toIocDiv_add_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a (b + p) = toIocDiv hp a b + 1
@[simp]
theorem toIocDiv_add_right' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp (a + p) b = toIocDiv hp a b - 1
@[simp]
theorem toIcoDiv_add_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1
@[simp]
theorem toIcoDiv_add_left' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1
@[simp]
theorem toIocDiv_add_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a (p + b) = toIocDiv hp a b + 1
@[simp]
theorem toIocDiv_add_left' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp (p + a) b = toIocDiv hp a b - 1
@[simp]
theorem toIcoDiv_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1
@[simp]
theorem toIcoDiv_sub' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1
@[simp]
theorem toIocDiv_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a (b - p) = toIocDiv hp a b - 1
@[simp]
theorem toIocDiv_sub' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp (a - p) b = toIocDiv hp a b + 1
theorem toIcoDiv_sub_eq_toIcoDiv_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b
theorem toIocDiv_sub_eq_toIocDiv_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIocDiv hp a (b - c) = toIocDiv hp (a + c) b
theorem toIcoDiv_sub_eq_toIcoDiv_add' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)
theorem toIocDiv_sub_eq_toIocDiv_add' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIocDiv hp (a - c) b = toIocDiv hp a (b + c)
theorem toIcoDiv_neg {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
theorem toIcoDiv_neg' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)
theorem toIocDiv_neg {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
theorem toIocDiv_neg' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)
@[simp]
theorem toIcoMod_add_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoMod hp a (b + m p) = toIcoMod hp a b
@[simp]
theorem toIcoMod_add_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoMod hp (a + m p) b = toIcoMod hp a b + m p
@[simp]
theorem toIocMod_add_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocMod hp a (b + m p) = toIocMod hp a b
@[simp]
theorem toIocMod_add_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocMod hp (a + m p) b = toIocMod hp a b + m p
@[simp]
theorem toIcoMod_zsmul_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoMod hp a (m p + b) = toIcoMod hp a b
@[simp]
theorem toIcoMod_zsmul_add' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoMod hp (m p + a) b = m p + toIcoMod hp a b
@[simp]
theorem toIocMod_zsmul_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocMod hp a (m p + b) = toIocMod hp a b
@[simp]
theorem toIocMod_zsmul_add' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocMod hp (m p + a) b = m p + toIocMod hp a b
@[simp]
theorem toIcoMod_sub_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoMod hp a (b - m p) = toIcoMod hp a b
@[simp]
theorem toIcoMod_sub_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIcoMod hp (a - m p) b = toIcoMod hp a b - m p
@[simp]
theorem toIocMod_sub_zsmul {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocMod hp a (b - m p) = toIocMod hp a b
@[simp]
theorem toIocMod_sub_zsmul' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (m : ) :
toIocMod hp (a - m p) b = toIocMod hp a b - m p
@[simp]
theorem toIcoMod_add_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a (b + p) = toIcoMod hp a b
@[simp]
theorem toIcoMod_add_right' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp (a + p) b = toIcoMod hp a b + p
@[simp]
theorem toIocMod_add_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a (b + p) = toIocMod hp a b
@[simp]
theorem toIocMod_add_right' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp (a + p) b = toIocMod hp a b + p
@[simp]
theorem toIcoMod_add_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a (p + b) = toIcoMod hp a b
@[simp]
theorem toIcoMod_add_left' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp (p + a) b = p + toIcoMod hp a b
@[simp]
theorem toIocMod_add_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a (p + b) = toIocMod hp a b
@[simp]
theorem toIocMod_add_left' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp (p + a) b = p + toIocMod hp a b
@[simp]
theorem toIcoMod_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a (b - p) = toIcoMod hp a b
@[simp]
theorem toIcoMod_sub' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp (a - p) b = toIcoMod hp a b - p
@[simp]
theorem toIocMod_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a (b - p) = toIocMod hp a b
@[simp]
theorem toIocMod_sub' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp (a - p) b = toIocMod hp a b - p
theorem toIcoMod_sub_eq_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c
theorem toIocMod_sub_eq_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIocMod hp a (b - c) = toIocMod hp (a + c) b - c
theorem toIcoMod_add_right_eq_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c
theorem toIocMod_add_right_eq_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) :
toIocMod hp a (b + c) = toIocMod hp (a - c) b + c
theorem toIcoMod_neg {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a (-b) = p - toIocMod hp (-a) b
theorem toIcoMod_neg' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp (-a) b = p - toIocMod hp a (-b)
theorem toIocMod_neg {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a (-b) = p - toIcoMod hp (-a) b
theorem toIocMod_neg' {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp (-a) b = p - toIcoMod hp a (-b)
theorem toIcoMod_eq_toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {c : α} :
toIcoMod hp a b = toIcoMod hp a c ∃ (n : ), c - b = n p
theorem toIocMod_eq_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {c : α} :
toIocMod hp a b = toIocMod hp a c ∃ (n : ), c - b = n p
theorem AddCommGroup.modEq_iff_toIcoMod_eq_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p] toIcoMod hp a b = a
theorem AddCommGroup.modEq_iff_toIocMod_eq_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p] toIocMod hp a b = a + p
theorem AddCommGroup.ModEq.toIcoMod_eq_left {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p]toIcoMod hp a b = a

Alias of the forward direction of AddCommGroup.modEq_iff_toIcoMod_eq_left.

theorem AddCommGroup.ModEq.toIcoMod_eq_right {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p]toIocMod hp a b = a + p

Alias of the forward direction of AddCommGroup.modEq_iff_toIocMod_eq_right.

theorem AddCommGroup.tfae_modEq {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
List.TFAE [a b [PMOD p], ∀ (z : ), b - z pSet.Ioo a (a + p), toIcoMod hp a b toIocMod hp a b, toIcoMod hp a b + p = toIocMod hp a b]
theorem AddCommGroup.modEq_iff_not_forall_mem_Ioo_mod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p] ∀ (z : ), b - z pSet.Ioo a (a + p)
theorem AddCommGroup.modEq_iff_toIcoMod_ne_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p] toIcoMod hp a b toIocMod hp a b
theorem AddCommGroup.modEq_iff_toIcoMod_add_period_eq_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p] toIcoMod hp a b + p = toIocMod hp a b
theorem AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
¬a b [PMOD p] toIcoMod hp a b = toIocMod hp a b
theorem AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
¬a b [PMOD p] toIcoDiv hp a b = toIocDiv hp a b
theorem AddCommGroup.modEq_iff_toIcoDiv_eq_toIocDiv_add_one {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
a b [PMOD p] toIcoDiv hp a b = toIocDiv hp a b + 1
@[simp]
theorem toIcoMod_inj {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {c : α} :
toIcoMod hp c a = toIcoMod hp c b a b [PMOD p]

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

theorem AddCommGroup.ModEq.toIcoMod_eq_toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} {c : α} :
a b [PMOD p]toIcoMod hp c a = toIcoMod hp c b

Alias of the reverse direction of toIcoMod_inj.

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

theorem Ico_eq_locus_Ioc_eq_iUnion_Ioo {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} :
{b : α | toIcoMod hp a b = toIocMod hp a b} = ⋃ (z : ), Set.Ioo (a + z p) (a + p + z p)
theorem toIocDiv_wcovBy_toIcoDiv {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a b ⩿ toIcoDiv hp a b
theorem toIcoMod_le_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a b toIocMod hp a b
theorem toIocMod_le_toIcoMod_add {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a b toIcoMod hp a b + p
theorem toIcoMod_eq_self {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
toIcoMod hp a b = b b Set.Ico a (a + p)
theorem toIocMod_eq_self {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) {a : α} {b : α} :
toIocMod hp a b = b b Set.Ioc a (a + p)
@[simp]
theorem toIcoMod_toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a₁ : α) (a₂ : α) (b : α) :
toIcoMod hp a₁ (toIcoMod hp a₂ b) = toIcoMod hp a₁ b
@[simp]
theorem toIcoMod_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a₁ : α) (a₂ : α) (b : α) :
toIcoMod hp a₁ (toIocMod hp a₂ b) = toIcoMod hp a₁ b
@[simp]
theorem toIocMod_toIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a₁ : α) (a₂ : α) (b : α) :
toIocMod hp a₁ (toIocMod hp a₂ b) = toIocMod hp a₁ b
@[simp]
theorem toIocMod_toIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a₁ : α) (a₂ : α) (b : α) :
toIocMod hp a₁ (toIcoMod hp a₂ b) = toIocMod hp a₁ b
theorem toIcoMod_periodic {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
theorem toIocMod_periodic {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
theorem toIcoMod_zero_sub_comm {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)
theorem toIocMod_zero_sub_comm {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)
theorem toIcoDiv_eq_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a b = toIcoDiv hp 0 (b - a)
theorem toIocDiv_eq_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a b = toIocDiv hp 0 (b - a)
theorem toIcoMod_eq_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
theorem toIocMod_eq_sub {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a b = toIocMod hp 0 (b - a) + a
theorem toIcoMod_add_toIocMod_zero {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p
theorem toIocMod_add_toIcoMod_zero {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p
@[simp]
theorem QuotientAddGroup.equivIcoMod_symm_apply {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (x : (Set.Ico a (a + p))) :
().symm x = x
def QuotientAddGroup.equivIcoMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
(Set.Ico a (a + p))

toIcoMod as an equiv from the quotient.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem QuotientAddGroup.equivIcoMod_coe {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
() b = { val := toIcoMod hp a b, property := }
@[simp]
theorem QuotientAddGroup.equivIcoMod_zero {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
() 0 = { val := toIcoMod hp a 0, property := }
@[simp]
theorem QuotientAddGroup.equivIocMod_symm_apply {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (x : (Set.Ioc a (a + p))) :
().symm x = x
def QuotientAddGroup.equivIocMod {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
(Set.Ioc a (a + p))

toIocMod as an equiv from the quotient.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem QuotientAddGroup.equivIocMod_coe {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) (b : α) :
() b = { val := toIocMod hp a b, property := }
@[simp]
theorem QuotientAddGroup.equivIocMod_zero {α : Type u_1} [hα : ] {p : α} (hp : 0 < p) (a : α) :
() 0 = { val := toIocMod hp a 0, property := }

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

Equations
• One or more equations did not get rendered due to their size.
theorem QuotientAddGroup.btw_coe_iff' {α : Type u_1} [hα : ] {p : α} [hp' : Fact (0 < p)] {x₁ : α} {x₂ : α} {x₃ : α} :
btw x₁ x₂ x₃ toIcoMod 0 (x₂ - x₁) toIocMod 0 (x₃ - x₁)
theorem QuotientAddGroup.btw_coe_iff {α : Type u_1} [hα : ] {p : α} [hp' : Fact (0 < p)] {x₁ : α} {x₂ : α} {x₃ : α} :
btw x₁ x₂ x₃ toIcoMod x₁ x₂ toIocMod x₁ x₃
instance QuotientAddGroup.circularPreorder {α : Type u_1} [hα : ] {p : α} [hp' : Fact (0 < p)] :
Equations
instance QuotientAddGroup.circularOrder {α : Type u_1} [hα : ] {p : α} [hp' : Fact (0 < p)] :
Equations

### Connections to Int.floor and Int.fract#

theorem toIcoDiv_eq_floor {α : Type u_1} [] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoDiv hp a b = (b - a) / p
theorem toIocDiv_eq_neg_floor {α : Type u_1} [] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocDiv hp a b = -(a + p - b) / p
theorem toIcoDiv_zero_one {α : Type u_1} [] (b : α) :
toIcoDiv 0 b = b
theorem toIcoMod_eq_add_fract_mul {α : Type u_1} [] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIcoMod hp a b = a + Int.fract ((b - a) / p) * p
theorem toIcoMod_eq_fract_mul {α : Type u_1} [] {p : α} (hp : 0 < p) (b : α) :
toIcoMod hp 0 b = Int.fract (b / p) * p
theorem toIocMod_eq_sub_fract_mul {α : Type u_1} [] {p : α} (hp : 0 < p) (a : α) (b : α) :
toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p
theorem toIcoMod_zero_one {α : Type u_1} [] (b : α) :
toIcoMod 0 b =

### Lemmas about unions of translates of intervals #

theorem iUnion_Ioc_add_zsmul {α : Type u_1} [] {p : α} (hp : 0 < p) (a : α) :
⋃ (n : ), Set.Ioc (a + n p) (a + (n + 1) p) = Set.univ
theorem iUnion_Ico_add_zsmul {α : Type u_1} [] {p : α} (hp : 0 < p) (a : α) :
⋃ (n : ), Set.Ico (a + n p) (a + (n + 1) p) = Set.univ
theorem iUnion_Icc_add_zsmul {α : Type u_1} [] {p : α} (hp : 0 < p) (a : α) :
⋃ (n : ), Set.Icc (a + n p) (a + (n + 1) p) = Set.univ
theorem iUnion_Ioc_zsmul {α : Type u_1} [] {p : α} (hp : 0 < p) :
⋃ (n : ), Set.Ioc (n p) ((n + 1) p) = Set.univ
theorem iUnion_Ico_zsmul {α : Type u_1} [] {p : α} (hp : 0 < p) :
⋃ (n : ), Set.Ico (n p) ((n + 1) p) = Set.univ
theorem iUnion_Icc_zsmul {α : Type u_1} [] {p : α} (hp : 0 < p) :
⋃ (n : ), Set.Icc (n p) ((n + 1) p) = Set.univ
theorem iUnion_Ioc_add_intCast {α : Type u_1} [] (a : α) :
⋃ (n : ), Set.Ioc (a + n) (a + n + 1) = Set.univ
theorem iUnion_Ico_add_intCast {α : Type u_1} [] (a : α) :
⋃ (n : ), Set.Ico (a + n) (a + n + 1) = Set.univ
theorem iUnion_Icc_add_intCast {α : Type u_1} [] (a : α) :
⋃ (n : ), Set.Icc (a + n) (a + n + 1) = Set.univ
theorem iUnion_Ioc_intCast (α : Type u_1) [] :
⋃ (n : ), Set.Ioc (n) (n + 1) = Set.univ
theorem iUnion_Ico_intCast (α : Type u_1) [] :
⋃ (n : ), Set.Ico (n) (n + 1) = Set.univ
theorem iUnion_Icc_intCast (α : Type u_1) [] :
⋃ (n : ), Set.Icc (n) (n + 1) = Set.univ