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} [LinearOrderedAddCommGroup α] [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

• toIcoDiv hp a b = Exists.choose ⋯

theorem sub_toIcoDiv_zsmul_mem_Ico {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [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

• toIocDiv hp a b = Exists.choose ⋯

theorem sub_toIocDiv_zsmul_mem_Ioc {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : α

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

Equations

• toIcoMod hp a b = b - toIcoDiv hp a b • p

def toIocMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : α

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

Equations

• toIocMod hp a b = b - toIocDiv hp a b • p

theorem toIcoMod_mem_Ico {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a b ∈ Set.Ico a (a + p)

theorem toIcoMod_mem_Ico' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (b : α) : toIcoMod hp 0 b ∈ Set.Ico 0 p

theorem toIocMod_mem_Ioc {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a b ∈ Set.Ioc a (a + p)

theorem left_le_toIcoMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : a ≤ toIcoMod hp a b

theorem left_lt_toIocMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : a < toIocMod hp a b

theorem toIcoMod_lt_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a b < a + p

theorem toIocMod_le_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a b ≤ a + p

@[simp]

theorem self_sub_toIcoDiv_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a b • p - b = -toIocMod hp a b

@[simp]

theorem toIcoMod_sub_self {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a b - b = -toIcoDiv hp a b • p

@[simp]

theorem toIocMod_sub_self {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a b - b = -toIocDiv hp a b • p

@[simp]

theorem self_sub_toIcoMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : b - toIcoMod hp a b = toIcoDiv hp a b • p

@[simp]

theorem self_sub_toIocMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a b • p + toIocMod hp a b = b

theorem toIcoMod_eq_iff {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIcoDiv hp a a = 0

@[simp]

theorem toIocDiv_apply_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIocDiv hp a a = -1

@[simp]

theorem toIcoMod_apply_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIcoMod hp a a = a

@[simp]

theorem toIocMod_apply_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIocMod hp a a = a + p

theorem toIcoDiv_apply_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIcoDiv hp a (a + p) = 1

theorem toIocDiv_apply_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIocDiv hp a (a + p) = 0

theorem toIcoMod_apply_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIcoMod hp a (a + p) = a

theorem toIocMod_apply_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : toIocMod hp a (a + p) = a + p

@[simp]

theorem toIcoDiv_add_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1

@[simp]

theorem toIcoDiv_add_right' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1

@[simp]

theorem toIocDiv_add_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a (b + p) = toIocDiv hp a b + 1

@[simp]

theorem toIocDiv_add_right' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp (a + p) b = toIocDiv hp a b - 1

@[simp]

theorem toIcoDiv_add_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1

@[simp]

theorem toIcoDiv_add_left' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1

@[simp]

theorem toIocDiv_add_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a (p + b) = toIocDiv hp a b + 1

@[simp]

theorem toIocDiv_add_left' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp (p + a) b = toIocDiv hp a b - 1

@[simp]

theorem toIcoDiv_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1

@[simp]

theorem toIcoDiv_sub' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1

@[simp]

theorem toIocDiv_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a (b - p) = toIocDiv hp a b - 1

@[simp]

theorem toIocDiv_sub' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) : toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

theorem toIcoDiv_neg {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

theorem toIcoDiv_neg' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)

theorem toIocDiv_neg {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)

theorem toIocDiv_neg' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)

@[simp]

theorem toIcoMod_add_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a (b + p) = toIcoMod hp a b

@[simp]

theorem toIcoMod_add_right' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp (a + p) b = toIcoMod hp a b + p

@[simp]

theorem toIocMod_add_right {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a (b + p) = toIocMod hp a b

@[simp]

theorem toIocMod_add_right' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp (a + p) b = toIocMod hp a b + p

@[simp]

theorem toIcoMod_add_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a (p + b) = toIcoMod hp a b

@[simp]

theorem toIcoMod_add_left' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp (p + a) b = p + toIcoMod hp a b

@[simp]

theorem toIocMod_add_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a (p + b) = toIocMod hp a b

@[simp]

theorem toIocMod_add_left' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp (p + a) b = p + toIocMod hp a b

@[simp]

theorem toIcoMod_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a (b - p) = toIcoMod hp a b

@[simp]

theorem toIcoMod_sub' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp (a - p) b = toIcoMod hp a b - p

@[simp]

theorem toIocMod_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a (b - p) = toIocMod hp a b

@[simp]

theorem toIocMod_sub' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp (a - p) b = toIocMod hp a b - p

theorem toIcoMod_sub_eq_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) (c : α) : toIocMod hp a (b + c) = toIocMod hp (a - c) b + c

theorem toIcoMod_neg {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a (-b) = p - toIocMod hp (-a) b

theorem toIcoMod_neg' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp (-a) b = p - toIocMod hp a (-b)

theorem toIocMod_neg {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a (-b) = p - toIcoMod hp (-a) b

theorem toIocMod_neg' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp (-a) b = p - toIcoMod hp a (-b)

theorem toIcoMod_eq_toIcoMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a : α} {b : α} {c : α} : toIocMod hp a b = toIocMod hp a c ↔ ∃ (n : ℤ), c - b = n • p

Links between the Ico and Ioc variants applied to the same element

theorem AddCommGroup.modEq_iff_toIcoMod_eq_left {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : List.TFAE [a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a : α} {b : α} : a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

theorem AddCommGroup.modEq_iff_toIcoMod_ne_toIocMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b

theorem toIcoMod_le_toIocMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a b ≤ toIocMod hp a b

theorem toIocMod_le_toIcoMod_add {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a b ≤ toIcoMod hp a b + p

theorem toIcoMod_eq_self {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a : α} {b : α} : toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)

theorem toIocMod_eq_self {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a : α} {b : α} : toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)

@[simp]

theorem toIcoMod_toIcoMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a₁ : α) (a₂ : α) (b : α) : toIocMod hp a₁ (toIcoMod hp a₂ b) = toIocMod hp a₁ b

theorem toIcoMod_periodic {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : Function.Periodic (toIcoMod hp a) p

theorem toIocMod_periodic {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : Function.Periodic (toIocMod hp a) p

theorem toIcoMod_zero_sub_comm {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)

theorem toIcoDiv_eq_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp a b = toIcoDiv hp 0 (b - a)

theorem toIocDiv_eq_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a b = toIocDiv hp 0 (b - a)

theorem toIcoMod_eq_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoMod hp a b = toIcoMod hp 0 (b - a) + a

theorem toIocMod_eq_sub {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocMod hp a b = toIocMod hp 0 (b - a) + a

theorem toIcoMod_add_toIocMod_zero {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (x : ↑(Set.Ico a (a + p))) : (QuotientAddGroup.equivIcoMod hp a).symm x = ↑↑x

def QuotientAddGroup.equivIcoMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ ↑(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.

@[simp]

theorem QuotientAddGroup.equivIcoMod_coe {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : (QuotientAddGroup.equivIcoMod hp a) ↑b = { val := toIcoMod hp a b, property := ⋯ }

@[simp]

theorem QuotientAddGroup.equivIcoMod_zero {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : (QuotientAddGroup.equivIcoMod hp a) 0 = { val := toIcoMod hp a 0, property := ⋯ }

@[simp]

theorem QuotientAddGroup.equivIocMod_symm_apply {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (x : ↑(Set.Ioc a (a + p))) : (QuotientAddGroup.equivIocMod hp a).symm x = ↑↑x

def QuotientAddGroup.equivIocMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ ↑(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.

@[simp]

theorem QuotientAddGroup.equivIocMod_coe {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) : (QuotientAddGroup.equivIocMod hp a) ↑b = { val := toIocMod hp a b, property := ⋯ }

@[simp]

theorem QuotientAddGroup.equivIocMod_zero {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) : (QuotientAddGroup.equivIocMod hp a) 0 = { val := toIocMod hp a 0, property := ⋯ }

The circular order structure on α ⧸ AddSubgroup.zmultiples p

instance QuotientAddGroup.instBtwQuotientAddSubgroupToAddGroupToAddCommGroupToOrderedAddCommGroupInstHasQuotientAddSubgroupZmultiples {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} [hp' : Fact (0 < p)] : Btw (α ⧸ AddSubgroup.zmultiples p)

Equations

• One or more equations did not get rendered due to their size.

theorem QuotientAddGroup.btw_coe_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} [hp' : Fact (0 < p)] {x₁ : α} {x₂ : α} {x₃ : α} : btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃

instance QuotientAddGroup.circularPreorder {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} [hp' : Fact (0 < p)] : CircularPreorder (α ⧸ AddSubgroup.zmultiples p)

Equations

• QuotientAddGroup.circularPreorder = CircularPreorder.mk ⋯ ⋯ ⋯ ⋯

instance QuotientAddGroup.circularOrder {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} [hp' : Fact (0 < p)] : CircularOrder (α ⧸ AddSubgroup.zmultiples p)

Equations

• QuotientAddGroup.circularOrder = let __src := QuotientAddGroup.circularPreorder; CircularOrder.mk ⋯

Connections to Int.floor and Int.fract

theorem toIcoDiv_eq_floor {α : Type u_1} [LinearOrderedField α] [FloorRing α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIcoDiv hp a b = ⌊(b - a) / p⌋

theorem toIocDiv_eq_neg_floor {α : Type u_1} [LinearOrderedField α] [FloorRing α] {p : α} (hp : 0 < p) (a : α) (b : α) : toIocDiv hp a b = -⌊(a + p - b) / p⌋

theorem toIcoDiv_zero_one {α : Type u_1} [LinearOrderedField α] [FloorRing α] (b : α) : toIcoDiv ⋯ 0 b = ⌊b⌋

theorem toIcoMod_eq_add_fract_mul {α : Type u_1} [LinearOrderedField α] [FloorRing α] {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} [LinearOrderedField α] [FloorRing α] {p : α} (hp : 0 < p) (b : α) : toIcoMod hp 0 b = Int.fract (b / p) * p

theorem toIocMod_eq_sub_fract_mul {α : Type u_1} [LinearOrderedField α] [FloorRing α] {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} [LinearOrderedField α] [FloorRing α] (b : α) : toIcoMod ⋯ 0 b = Int.fract b

Lemmas about unions of translates of intervals

theorem iUnion_Ioc_add_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {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} [LinearOrderedAddCommGroup α] [Archimedean α] {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} [LinearOrderedAddCommGroup α] [Archimedean α] {p : α} (hp : 0 < p) (a : α) : ⋃ (n : ℤ), Set.Icc (a + n • p) (a + (n + 1) • p) = Set.univ

theorem iUnion_Ioc_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {p : α} (hp : 0 < p) : ⋃ (n : ℤ), Set.Ioc (n • p) ((n + 1) • p) = Set.univ

theorem iUnion_Ico_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {p : α} (hp : 0 < p) : ⋃ (n : ℤ), Set.Ico (n • p) ((n + 1) • p) = Set.univ

theorem iUnion_Icc_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {p : α} (hp : 0 < p) : ⋃ (n : ℤ), Set.Icc (n • p) ((n + 1) • p) = Set.univ

theorem iUnion_Ioc_add_intCast {α : Type u_1} [LinearOrderedRing α] [Archimedean α] (a : α) : ⋃ (n : ℤ), Set.Ioc (a + ↑n) (a + ↑n + 1) = Set.univ

theorem iUnion_Ico_add_intCast {α : Type u_1} [LinearOrderedRing α] [Archimedean α] (a : α) : ⋃ (n : ℤ), Set.Ico (a + ↑n) (a + ↑n + 1) = Set.univ

theorem iUnion_Icc_add_intCast {α : Type u_1} [LinearOrderedRing α] [Archimedean α] (a : α) : ⋃ (n : ℤ), Set.Icc (a + ↑n) (a + ↑n + 1) = Set.univ

theorem iUnion_Ioc_intCast (α : Type u_1) [LinearOrderedRing α] [Archimedean α] : ⋃ (n : ℤ), Set.Ioc (↑n) (↑n + 1) = Set.univ

theorem iUnion_Ico_intCast (α : Type u_1) [LinearOrderedRing α] [Archimedean α] : ⋃ (n : ℤ), Set.Ico (↑n) (↑n + 1) = Set.univ

theorem iUnion_Icc_intCast (α : Type u_1) [LinearOrderedRing α] [Archimedean α] : ⋃ (n : ℤ), Set.Icc (↑n) (↑n + 1) = Set.univ