Documentation

Mathlib.Algebra.Order.Floor

Floor and ceil #

Summary #

We define the natural- and integer-valued floor and ceil functions on linearly ordered rings.

Main Definitions #

Notations #

The index in the notations for Nat.floor and Nat.ceil is used in analogy to the notation for nnnorm.

TODO #

LinearOrderedRing/LinearOrderedSemiring can be relaxed to OrderedRing/OrderedSemiring in many lemmas.

Tags #

rounding, floor, ceil

Floor semiring #

class FloorSemiring (α : Type u_4) [OrderedSemiring α] :
Type u_4

A FloorSemiring is an ordered semiring over α with a function floor : α → ℕ satisfying ∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x). Note that many lemmas require a LinearOrder. Please see the above TODO.

Instances
    theorem FloorSemiring.floor_of_neg {α : Type u_4} [OrderedSemiring α] [self : FloorSemiring α] {a : α} (ha : a < 0) :

    FloorSemiring.floor of a negative element is zero.

    theorem FloorSemiring.gc_floor {α : Type u_4} [OrderedSemiring α] [self : FloorSemiring α] {a : α} {n : } (ha : 0 a) :

    A natural number n is smaller than FloorSemiring.floor a iff its coercion to α is smaller than a.

    theorem FloorSemiring.gc_ceil {α : Type u_4} [OrderedSemiring α] [self : FloorSemiring α] :
    GaloisConnection FloorSemiring.ceil Nat.cast

    FloorSemiring.ceil is the lower adjoint of the coercion ↑ : ℕ → α.

    def Nat.floor {α : Type u_2} [OrderedSemiring α] [FloorSemiring α] :
    α

    ⌊a⌋₊ is the greatest natural n such that n ≤ a. If a is negative, then ⌊a⌋₊ = 0.

    Equations
    • Nat.floor = FloorSemiring.floor
    Instances For
      def Nat.ceil {α : Type u_2} [OrderedSemiring α] [FloorSemiring α] :
      α

      ⌈a⌉₊ is the least natural n such that a ≤ n

      Equations
      • Nat.ceil = FloorSemiring.ceil
      Instances For
        @[simp]
        theorem Nat.floor_nat :
        Nat.floor = id
        @[simp]
        theorem Nat.ceil_nat :
        Nat.ceil = id

        ⌊a⌋₊ is the greatest natural n such that n ≤ a. If a is negative, then ⌊a⌋₊ = 0.

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

          ⌈a⌉₊ is the least natural n such that a ≤ n

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Nat.le_floor_iff {α : Type u_2} [OrderedSemiring α] [FloorSemiring α] {a : α} {n : } (ha : 0 a) :
            n a⌋₊ n a
            theorem Nat.le_floor {α : Type u_2} [OrderedSemiring α] [FloorSemiring α] {a : α} {n : } (h : n a) :
            theorem Nat.gc_ceil_coe {α : Type u_2} [OrderedSemiring α] [FloorSemiring α] :
            GaloisConnection Nat.ceil Nat.cast
            @[simp]
            theorem Nat.ceil_le {α : Type u_2} [OrderedSemiring α] [FloorSemiring α] {a : α} {n : } :
            a⌉₊ n a n
            theorem Nat.floor_lt {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (ha : 0 a) :
            a⌋₊ < n a < n
            theorem Nat.floor_lt_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) :
            a⌋₊ < 1 a < 1
            theorem Nat.lt_of_floor_lt {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (h : a⌋₊ < n) :
            a < n
            theorem Nat.lt_one_of_floor_lt_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (h : a⌋₊ < 1) :
            a < 1
            theorem Nat.floor_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) :
            theorem Nat.lt_succ_floor {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) :
            a < a⌋₊.succ
            theorem Nat.lt_floor_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) :
            a < a⌋₊ + 1
            @[simp]
            theorem Nat.floor_natCast {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ) :
            n⌋₊ = n
            @[deprecated Nat.floor_natCast]
            theorem Nat.floor_coe {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ) :
            n⌋₊ = n

            Alias of Nat.floor_natCast.

            @[simp]
            @[simp]
            @[simp]
            theorem Nat.floor_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ) [n.AtLeastTwo] :
            theorem Nat.floor_of_nonpos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : a 0) :
            theorem Nat.floor_mono {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] :
            Monotone Nat.floor
            theorem Nat.floor_le_floor {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (hab : a b) :
            theorem Nat.le_floor_iff' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (hn : n 0) :
            n a⌋₊ n a
            @[simp]
            theorem Nat.one_le_floor_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (x : α) :
            theorem Nat.floor_lt' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (hn : n 0) :
            a⌋₊ < n a < n
            theorem Nat.floor_pos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} :
            theorem Nat.pos_of_floor_pos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (h : 0 < a⌋₊) :
            0 < a
            theorem Nat.lt_of_lt_floor {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (h : n < a⌋₊) :
            n < a
            theorem Nat.floor_le_of_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (h : a n) :
            theorem Nat.floor_le_one_of_le_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (h : a 1) :
            @[simp]
            theorem Nat.floor_eq_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} :
            a⌋₊ = 0 a < 1
            theorem Nat.floor_eq_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (ha : 0 a) :
            a⌋₊ = n n a a < n + 1
            theorem Nat.floor_eq_iff' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (hn : n 0) :
            a⌋₊ = n n a a < n + 1
            theorem Nat.floor_eq_on_Ico {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ) (a : α) :
            a Set.Ico (↑n) (n + 1)a⌋₊ = n
            theorem Nat.floor_eq_on_Ico' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ) (a : α) :
            a Set.Ico (↑n) (n + 1)a⌋₊ = n
            @[simp]
            theorem Nat.preimage_floor_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] :
            Nat.floor ⁻¹' {0} = Set.Iio 1
            theorem Nat.preimage_floor_of_ne_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {n : } (hn : n 0) :
            Nat.floor ⁻¹' {n} = Set.Ico (↑n) (n + 1)

            Ceil #

            theorem Nat.lt_ceil {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } :
            n < a⌉₊ n < a
            theorem Nat.add_one_le_ceil_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } :
            n + 1 a⌉₊ n < a
            @[simp]
            theorem Nat.one_le_ceil_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} :
            theorem Nat.le_ceil {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) :
            @[simp]
            theorem Nat.ceil_intCast {α : Type u_4} [LinearOrderedRing α] [FloorSemiring α] (z : ) :
            z⌉₊ = z.toNat
            @[simp]
            theorem Nat.ceil_natCast {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ) :
            n⌉₊ = n
            theorem Nat.ceil_le_ceil {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (hab : a b) :
            @[simp]
            @[simp]
            @[simp]
            theorem Nat.ceil_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ) [n.AtLeastTwo] :
            @[simp]
            theorem Nat.ceil_eq_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} :
            @[simp]
            theorem Nat.ceil_pos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} :
            0 < a⌉₊ 0 < a
            theorem Nat.lt_of_ceil_lt {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (h : a⌉₊ < n) :
            a < n
            theorem Nat.le_of_ceil_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (h : a⌉₊ n) :
            a n
            theorem Nat.floor_lt_ceil_of_lt_of_pos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (h : a < b) (h' : 0 < b) :
            theorem Nat.ceil_eq_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : } (hn : n 0) :
            a⌉₊ = n (n - 1) < a a n
            @[simp]
            theorem Nat.preimage_ceil_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] :
            Nat.ceil ⁻¹' {0} = Set.Iic 0
            theorem Nat.preimage_ceil_of_ne_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {n : } (hn : n 0) :
            Nat.ceil ⁻¹' {n} = Set.Ioc (n - 1) n

            Intervals #

            @[simp]
            theorem Nat.preimage_Ioo {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (ha : 0 a) :
            @[simp]
            theorem Nat.preimage_Ico {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} :
            @[simp]
            theorem Nat.preimage_Ioc {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
            @[simp]
            theorem Nat.preimage_Icc {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (hb : 0 b) :
            @[simp]
            theorem Nat.preimage_Ioi {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) :
            @[simp]
            theorem Nat.preimage_Ici {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} :
            @[simp]
            theorem Nat.preimage_Iio {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} :
            @[simp]
            theorem Nat.preimage_Iic {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) :
            theorem Nat.floor_add_nat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) (n : ) :
            theorem Nat.floor_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) :
            theorem Nat.floor_add_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) (n : ) [n.AtLeastTwo] :
            @[simp]
            theorem Nat.floor_sub_nat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ) :
            @[simp]
            theorem Nat.floor_sub_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) :
            @[simp]
            theorem Nat.floor_sub_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ) [n.AtLeastTwo] :
            theorem Nat.ceil_add_nat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) (n : ) :
            theorem Nat.ceil_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) :
            theorem Nat.ceil_add_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) (n : ) [n.AtLeastTwo] :
            theorem Nat.ceil_lt_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 a) :
            a⌉₊ < a + 1
            theorem Nat.ceil_add_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) (b : α) :
            theorem Nat.sub_one_lt_floor {α : Type u_2} [LinearOrderedRing α] [FloorSemiring α] (a : α) :
            a - 1 < a⌋₊
            theorem Nat.floor_div_nat {α : Type u_2} [LinearOrderedSemifield α] [FloorSemiring α] (a : α) (n : ) :
            theorem Nat.floor_div_ofNat {α : Type u_2} [LinearOrderedSemifield α] [FloorSemiring α] (a : α) (n : ) [n.AtLeastTwo] :
            theorem Nat.floor_div_eq_div {α : Type u_2} [LinearOrderedSemifield α] [FloorSemiring α] (m : ) (n : ) :
            m / n⌋₊ = m / n

            Natural division is the floor of field division.

            theorem Nat.mul_lt_floor {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} {b : α} (hb₀ : 0 < b) (hb : b < 1) (hba : b / (1 - b)⌉₊ a) :
            b * a < a⌋₊
            theorem Nat.ceil_lt_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} {b : α} (hb : 1 < b) (hba : (b - 1)⁻¹⌉₊ / b < a) :
            a⌉₊ < b * a
            theorem Nat.ceil_le_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} {b : α} (hb : 1 < b) (hba : (b - 1)⁻¹⌉₊ / b a) :
            a⌉₊ b * a
            theorem Nat.div_two_lt_floor {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} (ha : 1 a) :
            a / 2 < a⌋₊
            theorem Nat.ceil_lt_two_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} (ha : 2⁻¹ < a) :
            a⌉₊ < 2 * a
            theorem Nat.ceil_le_two_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} (ha : 2⁻¹ a) :
            a⌉₊ 2 * a

            There exists at most one FloorSemiring structure on a linear ordered semiring.

            Floor rings #

            class FloorRing (α : Type u_4) [LinearOrderedRing α] :
            Type u_4

            A FloorRing is a linear ordered ring over α with a function floor : α → ℤ satisfying ∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a).

            Instances
              theorem FloorRing.gc_coe_floor {α : Type u_4} [LinearOrderedRing α] [self : FloorRing α] :
              GaloisConnection Int.cast FloorRing.floor

              FloorRing.ceil is the upper adjoint of the coercion ↑ : ℤ → α.

              theorem FloorRing.gc_ceil_coe {α : Type u_4} [LinearOrderedRing α] [self : FloorRing α] :
              GaloisConnection FloorRing.ceil Int.cast

              FloorRing.ceil is the lower adjoint of the coercion ↑ : ℤ → α.

              Equations
              def FloorRing.ofFloor (α : Type u_4) [LinearOrderedRing α] (floor : α) (gc_coe_floor : GaloisConnection Int.cast floor) :

              A FloorRing constructor from the floor function alone.

              Equations
              • FloorRing.ofFloor α floor gc_coe_floor = { floor := floor, ceil := fun (a : α) => -floor (-a), gc_coe_floor := gc_coe_floor, gc_ceil_coe := }
              Instances For
                def FloorRing.ofCeil (α : Type u_4) [LinearOrderedRing α] (ceil : α) (gc_ceil_coe : GaloisConnection ceil Int.cast) :

                A FloorRing constructor from the ceil function alone.

                Equations
                • FloorRing.ofCeil α ceil gc_ceil_coe = { floor := fun (a : α) => -ceil (-a), ceil := ceil, gc_coe_floor := , gc_ceil_coe := gc_ceil_coe }
                Instances For
                  def Int.floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                  α

                  Int.floor a is the greatest integer z such that z ≤ a. It is denoted with ⌊a⌋.

                  Equations
                  • Int.floor = FloorRing.floor
                  Instances For
                    def Int.ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                    α

                    Int.ceil a is the smallest integer z such that a ≤ z. It is denoted with ⌈a⌉.

                    Equations
                    • Int.ceil = FloorRing.ceil
                    Instances For
                      def Int.fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                      α

                      Int.fract a, the fractional part of a, is a minus its floor.

                      Equations
                      Instances For
                        @[simp]
                        theorem Int.floor_int :
                        Int.floor = id
                        @[simp]
                        theorem Int.ceil_int :
                        Int.ceil = id
                        @[simp]
                        theorem Int.fract_int :
                        Int.fract = 0

                        Int.floor a is the greatest integer z such that z ≤ a. It is denoted with ⌊a⌋.

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

                          Int.ceil a is the smallest integer z such that a ≤ z. It is denoted with ⌈a⌉.

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

                            Floor #

                            theorem Int.gc_coe_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            GaloisConnection Int.cast Int.floor
                            theorem Int.le_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            z a z a
                            theorem Int.floor_lt {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            a < z a < z
                            theorem Int.floor_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a a
                            theorem Int.floor_nonneg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            0 a 0 a
                            @[simp]
                            theorem Int.floor_le_sub_one_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            a z - 1 a < z
                            @[simp]
                            theorem Int.floor_le_neg_one_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            a -1 a < 0
                            theorem Int.floor_nonpos {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : a 0) :
                            theorem Int.lt_succ_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a < a.succ
                            @[simp]
                            theorem Int.lt_floor_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a < a + 1
                            @[simp]
                            theorem Int.sub_one_lt_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a - 1 < a
                            @[simp]
                            theorem Int.floor_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ) :
                            z = z
                            @[simp]
                            theorem Int.floor_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) :
                            n = n
                            @[simp]
                            theorem Int.floor_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            @[simp]
                            theorem Int.floor_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            @[simp]
                            theorem Int.floor_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) [n.AtLeastTwo] :
                            theorem Int.floor_mono {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            Monotone Int.floor
                            theorem Int.floor_le_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} (hab : a b) :
                            theorem Int.floor_pos {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            0 < a 1 a
                            @[simp]
                            theorem Int.floor_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ) :
                            a + z = a + z
                            @[simp]
                            theorem Int.floor_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a + 1 = a + 1
                            theorem Int.le_floor_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) :
                            theorem Int.le_floor_add_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) :
                            @[simp]
                            theorem Int.floor_int_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ) (a : α) :
                            z + a = z + a
                            @[simp]
                            theorem Int.floor_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) :
                            a + n = a + n
                            @[simp]
                            theorem Int.floor_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) [n.AtLeastTwo] :
                            @[simp]
                            theorem Int.floor_nat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) (a : α) :
                            n + a = n + a
                            @[simp]
                            theorem Int.floor_ofNat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) [n.AtLeastTwo] (a : α) :
                            @[simp]
                            theorem Int.floor_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ) :
                            a - z = a - z
                            @[simp]
                            theorem Int.floor_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) :
                            a - n = a - n
                            @[simp]
                            theorem Int.floor_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a - 1 = a - 1
                            @[simp]
                            theorem Int.floor_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) [n.AtLeastTwo] :
                            theorem Int.abs_sub_lt_one_of_floor_eq_floor {α : Type u_4} [LinearOrderedCommRing α] [FloorRing α] {a : α} {b : α} (h : a = b) :
                            |a - b| < 1
                            theorem Int.floor_eq_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            a = z z a a < z + 1
                            @[simp]
                            theorem Int.floor_eq_zero_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            theorem Int.floor_eq_on_Ico {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) (a : α) :
                            a Set.Ico (↑n) (n + 1)a = n
                            theorem Int.floor_eq_on_Ico' {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) (a : α) :
                            a Set.Ico (↑n) (n + 1)a = n
                            @[simp]
                            theorem Int.preimage_floor_singleton {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (m : ) :
                            Int.floor ⁻¹' {m} = Set.Ico (↑m) (m + 1)

                            Fractional part #

                            @[simp]
                            theorem Int.self_sub_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.floor_add_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_add_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (m : ) :
                            Int.fract (a + m) = Int.fract a
                            @[simp]
                            theorem Int.fract_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (m : ) :
                            Int.fract (a + m) = Int.fract a
                            @[simp]
                            theorem Int.fract_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) [n.AtLeastTwo] :
                            @[simp]
                            theorem Int.fract_int_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (m : ) (a : α) :
                            Int.fract (m + a) = Int.fract a
                            @[simp]
                            theorem Int.fract_nat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) (a : α) :
                            Int.fract (n + a) = Int.fract a
                            @[simp]
                            theorem Int.fract_one_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_ofNat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) [n.AtLeastTwo] (a : α) :
                            @[simp]
                            theorem Int.fract_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (m : ) :
                            Int.fract (a - m) = Int.fract a
                            @[simp]
                            theorem Int.fract_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) :
                            Int.fract (a - n) = Int.fract a
                            @[simp]
                            theorem Int.fract_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) [n.AtLeastTwo] :
                            theorem Int.fract_add_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) :
                            theorem Int.fract_add_fract_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) :
                            @[simp]
                            theorem Int.self_sub_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_sub_self {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_nonneg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            theorem Int.fract_pos {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :

                            The fractional part of a is positive if and only if a ≠ ⌊a⌋.

                            theorem Int.fract_lt_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.fract_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            @[simp]
                            theorem Int.fract_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            theorem Int.abs_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            @[simp]
                            theorem Int.abs_one_sub_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            |1 - Int.fract a| = 1 - Int.fract a
                            @[simp]
                            theorem Int.fract_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ) :
                            Int.fract z = 0
                            @[simp]
                            theorem Int.fract_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) :
                            Int.fract n = 0
                            @[simp]
                            theorem Int.fract_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) [n.AtLeastTwo] :
                            theorem Int.fract_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            @[simp]
                            theorem Int.floor_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            theorem Int.fract_eq_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} :
                            Int.fract a = b 0 b b < 1 ∃ (z : ), a - b = z
                            theorem Int.fract_eq_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} :
                            Int.fract a = Int.fract b ∃ (z : ), a - b = z
                            @[simp]
                            theorem Int.fract_eq_self {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            Int.fract a = a 0 a a < 1
                            @[simp]
                            theorem Int.fract_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            theorem Int.fract_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) :
                            ∃ (z : ), Int.fract (a + b) - Int.fract a - Int.fract b = z
                            theorem Int.fract_neg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {x : α} (hx : Int.fract x 0) :
                            @[simp]
                            theorem Int.fract_neg_eq_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {x : α} :
                            theorem Int.fract_mul_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : ) :
                            ∃ (z : ), Int.fract a * b - Int.fract (a * b) = z
                            theorem Int.preimage_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (s : Set α) :
                            Int.fract ⁻¹' s = ⋃ (m : ), (fun (x : α) => x - m) ⁻¹' (s Set.Ico 0 1)
                            theorem Int.image_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (s : Set α) :
                            Int.fract '' s = ⋃ (m : ), (fun (x : α) => x - m) '' s Set.Ico 0 1
                            theorem Int.fract_div_mul_self_mem_Ico {k : Type u_4} [LinearOrderedField k] [FloorRing k] (a : k) (b : k) (ha : 0 < a) :
                            Int.fract (b / a) * a Set.Ico 0 a
                            theorem Int.fract_div_mul_self_add_zsmul_eq {k : Type u_4} [LinearOrderedField k] [FloorRing k] (a : k) (b : k) (ha : a 0) :
                            Int.fract (b / a) * a + b / a a = b
                            theorem Int.sub_floor_div_mul_nonneg {k : Type u_4} [LinearOrderedField k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) :
                            0 a - a / b * b
                            theorem Int.sub_floor_div_mul_lt {k : Type u_4} [LinearOrderedField k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) :
                            a - a / b * b < b
                            theorem Int.fract_div_natCast_eq_div_natCast_mod {k : Type u_4} [LinearOrderedField k] [FloorRing k] {m : } {n : } :
                            Int.fract (m / n) = (m % n) / n
                            theorem Int.fract_div_intCast_eq_div_intCast_mod {k : Type u_4} [LinearOrderedField k] [FloorRing k] {m : } {n : } :
                            Int.fract (m / n) = (m % n) / n

                            Ceil #

                            theorem Int.gc_ceil_coe {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            GaloisConnection Int.ceil Int.cast
                            theorem Int.ceil_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            a z a z
                            theorem Int.floor_neg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            theorem Int.ceil_neg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            theorem Int.lt_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            z < a z < a
                            @[simp]
                            theorem Int.add_one_le_ceil_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            z + 1 a z < a
                            @[simp]
                            theorem Int.one_le_ceil_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            1 a 0 < a
                            theorem Int.le_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a a
                            theorem Int.le_ceil_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            z a z - 1 < a
                            theorem Int.ceil_lt_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            a < z a z - 1
                            @[simp]
                            theorem Int.ceil_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ) :
                            z = z
                            @[simp]
                            theorem Int.ceil_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) :
                            n = n
                            @[simp]
                            theorem Int.ceil_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) [n.AtLeastTwo] :
                            theorem Int.ceil_mono {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            Monotone Int.ceil
                            theorem Int.ceil_le_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} (hab : a b) :
                            @[simp]
                            theorem Int.ceil_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ) :
                            a + z = a + z
                            @[simp]
                            theorem Int.ceil_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) :
                            a + n = a + n
                            @[simp]
                            theorem Int.ceil_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a + 1 = a + 1
                            @[simp]
                            theorem Int.ceil_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) [n.AtLeastTwo] :
                            @[simp]
                            theorem Int.ceil_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ) :
                            a - z = a - z
                            @[simp]
                            theorem Int.ceil_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) :
                            a - n = a - n
                            @[simp]
                            theorem Int.ceil_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a - 1 = a - 1
                            @[simp]
                            theorem Int.ceil_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ) [n.AtLeastTwo] :
                            theorem Int.ceil_lt_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            a < a + 1
                            theorem Int.ceil_add_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) :
                            theorem Int.ceil_add_ceil_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) :
                            @[simp]
                            theorem Int.ceil_pos {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            0 < a 0 < a
                            @[simp]
                            theorem Int.ceil_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            @[simp]
                            theorem Int.ceil_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                            theorem Int.ceil_nonneg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 a) :
                            theorem Int.ceil_eq_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : } {a : α} :
                            a = z z - 1 < a a z
                            @[simp]
                            theorem Int.ceil_eq_zero_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            a = 0 a Set.Ioc (-1) 0
                            theorem Int.ceil_eq_on_Ioc {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ) (a : α) :
                            a Set.Ioc (z - 1) za = z
                            theorem Int.ceil_eq_on_Ioc' {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ) (a : α) :
                            a Set.Ioc (z - 1) za = z
                            theorem Int.floor_le_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                            theorem Int.floor_lt_ceil_of_lt {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} (h : a < b) :
                            @[simp]
                            theorem Int.preimage_ceil_singleton {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (m : ) :
                            Int.ceil ⁻¹' {m} = Set.Ioc (m - 1) m
                            theorem Int.ceil_eq_add_one_sub_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : Int.fract a 0) :
                            a = a + 1 - Int.fract a
                            theorem Int.ceil_sub_self_eq {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : Int.fract a 0) :
                            a - a = 1 - Int.fract a
                            theorem Int.mul_lt_floor {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} {b : k} (hb₀ : 0 < b) (hb : b < 1) (hba : b / (1 - b) a) :
                            b * a < a
                            theorem Int.ceil_div_ceil_inv_sub_one {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 1 a) :
                            theorem Int.ceil_lt_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} {b : k} (hb : 1 < b) (hba : (b - 1)⁻¹ / b < a) :
                            a < b * a
                            theorem Int.ceil_le_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} {b : k} (hb : 1 < b) (hba : (b - 1)⁻¹ / b a) :
                            a b * a
                            theorem Int.div_two_lt_floor {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 1 a) :
                            a / 2 < a
                            theorem Int.ceil_lt_two_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 2⁻¹ < a) :
                            a < 2 * a
                            theorem Int.ceil_le_two_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 2⁻¹ a) :
                            a 2 * a

                            Intervals #

                            @[simp]
                            theorem Int.preimage_Ioo {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} :
                            @[simp]
                            theorem Int.preimage_Ico {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} :
                            @[simp]
                            theorem Int.preimage_Ioc {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} :
                            @[simp]
                            theorem Int.preimage_Icc {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} :
                            @[simp]
                            theorem Int.preimage_Ioi {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            @[simp]
                            theorem Int.preimage_Ici {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            @[simp]
                            theorem Int.preimage_Iio {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :
                            @[simp]
                            theorem Int.preimage_Iic {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} :

                            Round #

                            def round {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) :

                            round rounds a number to the nearest integer. round (1 / 2) = 1

                            Equations
                            Instances For
                              @[simp]
                              theorem round_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                              round 0 = 0
                              @[simp]
                              theorem round_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
                              round 1 = 1
                              @[simp]
                              theorem round_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) :
                              round n = n
                              @[simp]
                              theorem round_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) [n.AtLeastTwo] :
                              @[simp]
                              theorem round_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) :
                              round n = n
                              @[simp]
                              theorem round_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ) :
                              round (x + y) = round x + y
                              @[simp]
                              theorem round_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                              round (a + 1) = round a + 1
                              @[simp]
                              theorem round_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ) :
                              round (x - y) = round x - y
                              @[simp]
                              theorem round_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                              round (a - 1) = round a - 1
                              @[simp]
                              theorem round_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ) :
                              round (x + y) = round x + y
                              @[simp]
                              theorem round_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (n : ) [n.AtLeastTwo] :
                              @[simp]
                              theorem round_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ) :
                              round (x - y) = round x - y
                              @[simp]
                              theorem round_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (n : ) [n.AtLeastTwo] :
                              @[simp]
                              theorem round_int_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ) :
                              round (y + x) = y + round x
                              @[simp]
                              theorem round_nat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ) :
                              round (y + x) = y + round x
                              @[simp]
                              theorem round_ofNat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ) [n.AtLeastTwo] (x : α) :
                              theorem abs_sub_round_eq_min {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) :
                              |x - (round x)| = min (Int.fract x) (1 - Int.fract x)
                              theorem round_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (z : ) :
                              |x - (round x)| |x - z|
                              theorem round_eq {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
                              round x = x + 1 / 2
                              @[simp]
                              theorem round_two_inv {α : Type u_2} [LinearOrderedField α] [FloorRing α] :
                              @[simp]
                              theorem round_neg_two_inv {α : Type u_2} [LinearOrderedField α] [FloorRing α] :
                              @[simp]
                              theorem round_eq_zero_iff {α : Type u_2} [LinearOrderedField α] [FloorRing α] {x : α} :
                              round x = 0 x Set.Ico (-(1 / 2)) (1 / 2)
                              theorem abs_sub_round {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
                              |x - (round x)| 1 / 2
                              theorem abs_sub_round_div_natCast_eq {α : Type u_2} [LinearOrderedField α] [FloorRing α] {m : } {n : } :
                              |m / n - (round (m / n))| = (min (m % n) (n - m % n)) / n
                              theorem sub_half_lt_round {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
                              x - 1 / 2 < (round x)
                              theorem round_le_add_half {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
                              (round x) x + 1 / 2
                              theorem Nat.floor_congr {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] {a : α} {b : β} (h : ∀ (n : ), n a n b) :
                              theorem Nat.ceil_congr {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] {a : α} {b : β} (h : ∀ (n : ), a n b n) :
                              theorem Nat.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono f) (a : α) :
                              theorem Nat.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono f) (a : α) :
                              theorem Int.floor_congr {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] {a : α} {b : β} (h : ∀ (n : ), n a n b) :
                              theorem Int.ceil_congr {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] {a : α} {b : β} (h : ∀ (n : ), a n b n) :
                              theorem Int.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono f) (a : α) :
                              theorem Int.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono f) (a : α) :
                              theorem Int.map_fract {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono f) (a : α) :
                              Int.fract (f a) = f (Int.fract a)
                              theorem Int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [LinearOrderedField β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono f) (a : α) :
                              round (f a) = round a

                              A floor ring as a floor semiring #

                              @[instance 100]
                              Equations
                              • FloorRing.toFloorSemiring = { floor := fun (a : α) => a.toNat, ceil := fun (a : α) => a.toNat, floor_of_neg := , gc_floor := , gc_ceil := }
                              theorem Int.floor_toNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                              theorem Int.ceil_toNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
                              @[simp]
                              theorem Nat.floor_int :
                              Nat.floor = Int.toNat
                              @[simp]
                              theorem Nat.ceil_int :
                              Nat.ceil = Int.toNat
                              theorem Int.natCast_floor_eq_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 a) :
                              theorem Int.natCast_ceil_eq_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 a) :
                              theorem natCast_floor_eq_intCast_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 a) :
                              theorem natCast_ceil_eq_intCast_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 a) :
                              @[deprecated Int.natCast_floor_eq_floor]
                              theorem Int.ofNat_floor_eq_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 a) :

                              Alias of Int.natCast_floor_eq_floor.

                              @[deprecated Int.natCast_ceil_eq_ceil]
                              theorem Int.ofNat_ceil_eq_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 a) :

                              Alias of Int.natCast_ceil_eq_ceil.

                              There exists at most one FloorRing structure on a given linear ordered ring.

                              Extension for the positivity tactic: Int.floor is nonnegative if its input is.

                              Instances For

                                Extension for the positivity tactic: Nat.ceil is positive if its input is.

                                Instances For

                                  Extension for the positivity tactic: Int.ceil is positive/nonnegative if its input is.

                                  Instances For