Documentation

Mathlib.Algebra.Order.ToIntervalMod

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 #

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
Instances For
    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
    Instances For
      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
      Instances For
        def toIocMod {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {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} [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
          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 : α) :
          theorem toIocMod_periodic {α : Type u_1} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) :
          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 : α) :

          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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) :
            ↑(QuotientAddGroup.equivIcoMod hp a) b = { val := toIcoMod hp a b, property := (_ : toIcoMod hp a b Set.Ico a (a + p)) }
            @[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 := (_ : toIcoMod hp a 0 Set.Ico a (a + p)) }
            @[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 : α) :

            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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a : α) (b : α) :
              ↑(QuotientAddGroup.equivIocMod hp a) b = { val := toIocMod hp a b, property := (_ : toIocMod hp a b Set.Ioc a (a + p)) }
              @[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 := (_ : toIocMod hp a 0 Set.Ioc a (a + p)) }

              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} [LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} [hp' : Fact (0 < p)] {x₁ : α} {x₂ : α} {x₃ : α} :
              btw x₁ x₂ x₃ toIcoMod (_ : 0 < p) 0 (x₂ - x₁) toIocMod (_ : 0 < p) 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 (_ : 0 < p) x₁ x₂ toIocMod (_ : 0 < p) x₁ x₃
              Equations
              • One or more equations did not get rendered due to their size.
              Equations

              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 < 1) 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 < 1) 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_int_cast {α : Type u_1} [LinearOrderedRing α] [Archimedean α] (a : α) :
              ⋃ (n : ), Set.Ioc (a + n) (a + n + 1) = Set.univ
              theorem iUnion_Ico_add_int_cast {α : Type u_1} [LinearOrderedRing α] [Archimedean α] (a : α) :
              ⋃ (n : ), Set.Ico (a + n) (a + n + 1) = Set.univ
              theorem iUnion_Icc_add_int_cast {α : Type u_1} [LinearOrderedRing α] [Archimedean α] (a : α) :
              ⋃ (n : ), Set.Icc (a + n) (a + n + 1) = Set.univ
              theorem iUnion_Ioc_int_cast (α : Type u_1) [LinearOrderedRing α] [Archimedean α] :
              ⋃ (n : ), Set.Ioc (n) (n + 1) = Set.univ
              theorem iUnion_Ico_int_cast (α : Type u_1) [LinearOrderedRing α] [Archimedean α] :
              ⋃ (n : ), Set.Ico (n) (n + 1) = Set.univ
              theorem iUnion_Icc_int_cast (α : Type u_1) [LinearOrderedRing α] [Archimedean α] :
              ⋃ (n : ), Set.Icc (n) (n + 1) = Set.univ