Documentation

Mathlib.Algebra.Order.Floor.Ring

Lemmas on Int.floor, Int.ceil and Int.fract #

This file contains basic results on the integer-valued floor and ceiling functions, as well as the fractional part operator.

TODO #

LinearOrderedRing can be relaxed to OrderedRing in many lemmas.

Tags #

rounding, floor, ceil

source
theorem Mathlib.Meta.Positivity.int_floor_nonneg {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} (ha : 0 ≤ a) :
0 ≤ ⌊a⌋
source
theorem Mathlib.Meta.Positivity.int_floor_nonneg_of_pos {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} (ha : 0 < a) :
0 ≤ ⌊a⌋
source
def Mathlib.Meta.Positivity.evalIntFloor :
PositivityExt

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Mathlib.Meta.Positivity.nat_ceil_pos {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} :
    0 < a → 0 < ⌈a⌉₊
    source
    def Mathlib.Meta.Positivity.evalNatCeil :
    PositivityExt

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

    Instances For
      source
      theorem Mathlib.Meta.Positivity.int_ceil_pos {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} :
      0 < a → 0 < ⌈a⌉
      source
      def Mathlib.Meta.Positivity.evalIntCeil :
      PositivityExt

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

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

        Floor rings #

        Floor #

        source
        @[deprecated Int.floor_lt (since := "2025-12-26")]
        theorem Int.floor_le_sub_one_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
        ⌊a⌋ ≤ z - 1 ↔ a < ↑z
        source
        @[simp]
        theorem Int.floor_le_neg_one_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        ⌊a⌋ ≤ -1 ↔ a < 0
        source
        theorem Int.lt_succ_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        a < ↑⌊a⌋.succ
        source
        @[simp]
        theorem Int.lt_floor_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        a < ↑⌊a⌋ + 1
        source
        theorem Int.floor_mono {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] :
        Monotone floor
        source
        theorem Int.floor_le_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} (hab : a ≤ b) :
        ⌊a⌋ ≤ ⌊b⌋
        source
        theorem Int.floor_pos {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        0 < ⌊a⌋ ↔ 1 ≤ a
        source
        theorem Int.floor_eq_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
        ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
        source
        @[simp]
        theorem Int.floor_eq_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        ⌊a⌋ = 0 ↔ a ∈ Set.Ico 0 1
        source
        theorem Int.floor_eq_on_Ico {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (n : ℤ) (a : R) :
        a ∈ Set.Ico (↑n) (↑n + 1) → ⌊a⌋ = n
        source
        theorem Int.floor_eq_on_Ico' {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (n : ℤ) (a : R) :
        a ∈ Set.Ico (↑n) (↑n + 1) → ↑⌊a⌋ = ↑n
        source
        @[simp]
        theorem Int.preimage_floor_singleton {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (m : ℤ) :
        floor ⁻¹' {m} = Set.Ico (↑m) (↑m + 1)
        source
        @[simp]
        theorem Int.sub_one_lt_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        a - 1 < ↑⌊a⌋
        source
        @[simp]
        theorem Int.floor_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (z : ℤ) :
        ⌊↑z⌋ = z
        source
        @[simp]
        theorem Int.floor_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) :
        ⌊↑n⌋ = ↑n
        source
        @[simp]
        theorem Int.floor_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] :
        ⌊0⌋ = 0
        source
        @[simp]
        theorem Int.floor_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] :
        ⌊1⌋ = 1
        source
        @[simp]
        theorem Int.floor_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) [n.AtLeastTwo] :
        ⌊OfNat.ofNat n⌋ = OfNat.ofNat n
        source
        @[simp]
        theorem Int.floor_add_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ) :
        ⌊a + ↑z⌋ = ⌊a⌋ + z
        source
        @[simp]
        theorem Int.floor_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌊a + 1⌋ = ⌊a⌋ + 1
        source
        theorem Int.le_floor_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a b : R) :
        ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
        source
        theorem Int.le_floor_add_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a b : R) :
        ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋
        source
        @[simp]
        theorem Int.floor_intCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (z : ℤ) (a : R) :
        ⌊↑z + a⌋ = z + ⌊a⌋
        source
        @[simp]
        theorem Int.floor_add_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) :
        ⌊a + ↑n⌋ = ⌊a⌋ + ↑n
        source
        @[simp]
        theorem Int.floor_add_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] :
        ⌊a + OfNat.ofNat n⌋ = ⌊a⌋ + OfNat.ofNat n
        source
        @[simp]
        theorem Int.floor_natCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) (a : R) :
        ⌊↑n + a⌋ = ↑n + ⌊a⌋
        source
        @[simp]
        theorem Int.floor_ofNat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) [n.AtLeastTwo] (a : R) :
        ⌊OfNat.ofNat n + a⌋ = OfNat.ofNat n + ⌊a⌋
        source
        @[simp]
        theorem Int.floor_sub_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ) :
        ⌊a - ↑z⌋ = ⌊a⌋ - z
        source
        @[simp]
        theorem Int.floor_sub_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) :
        ⌊a - ↑n⌋ = ⌊a⌋ - ↑n
        source
        @[simp]
        theorem Int.floor_sub_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌊a - 1⌋ = ⌊a⌋ - 1
        source
        @[simp]
        theorem Int.floor_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] :
        ⌊a - OfNat.ofNat n⌋ = ⌊a⌋ - OfNat.ofNat n
        source
        theorem Int.abs_sub_lt_one_of_floor_eq_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a b : R} (h : ⌊a⌋ = ⌊b⌋) :
        |a - b| < 1
        source
        theorem Int.floor_eq_self_iff_mem {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ↑⌊a⌋ = a ↔ a ∈ Set.range Int.cast
        source
        theorem Int.floor_lt_self_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a : R} :
        ↑⌊a⌋ < a ↔ a ∉ Set.range Int.cast
        source
        theorem Int.mul_cast_floor_div_cancel_of_pos {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℤ} (hn : 0 < n) (a : R) :
        ⌊a * ↑n⌋ / n = ⌊a⌋
        source
        theorem Int.mul_natCast_floor_div_cancel {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℕ} (hn : n ≠ 0) (a : R) :
        ⌊a * ↑n⌋ / ↑n = ⌊a⌋
        source
        theorem Int.mul_fract_eq_one_iff_exists_int {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {x k : R} (hk : 1 < k) :
        k * fract x = 1 ↔ ∃ (n : ℤ), k * x = k * ↑n + 1
        source
        theorem Int.cast_mul_floor_div_cancel_of_pos {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℤ} (hn : 0 < n) (a : R) :
        ⌊↑n * a⌋ / n = ⌊a⌋
        source
        theorem Int.natCast_mul_floor_div_cancel {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℕ} (hn : n ≠ 0) (a : R) :
        ⌊↑n * a⌋ / ↑n = ⌊a⌋
        source
        theorem Int.floor_div_cast_of_nonneg {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {n : ℤ} (hn : 0 ≤ n) (a : k) :
        ⌊a / ↑n⌋ = ⌊a⌋ / n
        source
        theorem Int.floor_div_natCast {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] (a : k) (n : ℕ) :
        ⌊a / ↑n⌋ = ⌊a⌋ / ↑n

        Fractional part #

        source
        @[simp]
        theorem Int.self_sub_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        a - ↑⌊a⌋ = fract a
        source
        @[simp]
        theorem Int.floor_add_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        ↑⌊a⌋ + fract a = a
        source
        @[simp]
        theorem Int.fract_add_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        fract a + ↑⌊a⌋ = a
        source
        @[simp]
        theorem Int.self_sub_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        a - fract a = ↑⌊a⌋
        source
        @[simp]
        theorem Int.fract_sub_self {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        fract a - a = -↑⌊a⌋
        source
        theorem Int.fract_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a b : R) :
        ∃ (z : ℤ), fract (a + b) - fract a - fract b = ↑z
        source
        @[simp]
        theorem Int.fract_add_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (m : ℤ) :
        fract (a + ↑m) = fract a
        source
        @[simp]
        theorem Int.fract_add_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (m : ℕ) :
        fract (a + ↑m) = fract a
        source
        @[simp]
        theorem Int.fract_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        fract (a + 1) = fract a
        source
        @[simp]
        theorem Int.fract_add_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] :
        fract (a + OfNat.ofNat n) = fract a
        source
        @[simp]
        theorem Int.fract_intCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (m : ℤ) (a : R) :
        fract (↑m + a) = fract a
        source
        @[simp]
        theorem Int.fract_natCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) (a : R) :
        fract (↑n + a) = fract a
        source
        @[simp]
        theorem Int.fract_one_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        fract (1 + a) = fract a
        source
        @[simp]
        theorem Int.fract_ofNat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) [n.AtLeastTwo] (a : R) :
        fract (OfNat.ofNat n + a) = fract a
        source
        @[simp]
        theorem Int.fract_sub_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (m : ℤ) :
        fract (a - ↑m) = fract a
        source
        @[simp]
        theorem Int.fract_sub_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) :
        fract (a - ↑n) = fract a
        source
        @[simp]
        theorem Int.fract_sub_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        fract (a - 1) = fract a
        source
        @[simp]
        theorem Int.fract_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] :
        fract (a - OfNat.ofNat n) = fract a
        source
        theorem Int.fract_add_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a b : R) :
        fract (a + b) ≤ fract a + fract b
        source
        theorem Int.fract_add_fract_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a b : R) :
        fract a + fract b ≤ fract (a + b) + 1
        source
        @[simp]
        theorem Int.fract_nonneg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        0 ≤ fract a
        source
        theorem Int.fract_pos {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsOrderedRing R] :
        0 < fract a ↔ a ≠ ↑⌊a⌋

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

        source
        theorem Int.fract_lt_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        fract a < 1
        source
        @[simp]
        theorem Int.fract_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] :
        fract 0 = 0
        source
        @[simp]
        theorem Int.fract_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] :
        fract 1 = 0
        source
        theorem Int.abs_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsOrderedRing R] :
        |fract a| = fract a
        source
        @[simp]
        theorem Int.abs_one_sub_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsOrderedRing R] :
        |1 - fract a| = 1 - fract a
        source
        @[simp]
        theorem Int.fract_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (z : ℤ) :
        fract ↑z = 0
        source
        @[simp]
        theorem Int.fract_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) :
        fract ↑n = 0
        source
        @[simp]
        theorem Int.fract_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) [n.AtLeastTwo] :
        fract (OfNat.ofNat n) = 0
        source
        theorem Int.fract_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        fract ↑⌊a⌋ = 0
        source
        @[simp]
        theorem Int.floor_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌊fract a⌋ = 0
        source
        theorem Int.fract_eq_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a b : R} :
        fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ (z : ℤ), a - b = ↑z
        source
        theorem Int.fract_eq_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a b : R} :
        fract a = fract b ↔ ∃ (z : ℤ), a - b = ↑z
        source
        @[simp]
        theorem Int.fract_eq_self {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a : R} :
        fract a = a ↔ 0 ≤ a ∧ a < 1
        source
        @[simp]
        theorem Int.fract_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        fract (fract a) = fract a
        source
        theorem Int.fract_eq_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a : R} :
        fract a = 0 ↔ a ∈ Set.range Int.cast
        source
        theorem Int.fract_ne_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a : R} :
        fract a ≠ 0 ↔ a ∉ Set.range Int.cast
        source
        theorem Int.fract_neg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {x : R} (hx : fract x ≠ 0) :
        fract (-x) = 1 - fract x
        source
        @[simp]
        theorem Int.fract_neg_eq_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {x : R} :
        fract (-x) = 0 ↔ fract x = 0
        source
        theorem Int.fract_mul_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (b : ℕ) :
        ∃ (z : ℤ), fract a * ↑b - fract (a * ↑b) = ↑z
        source
        theorem Int.preimage_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (s : Set R) :
        fract ⁻¹' s = ⋃ (m : ℤ), (fun (x : R) => x - ↑m) ⁻¹' (s ∩ Set.Ico 0 1)
        source
        theorem Int.image_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (s : Set R) :
        fract '' s = ⋃ (m : ℤ), (fun (x : R) => x - ↑m) '' s ∩ Set.Ico 0 1
        source
        theorem Int.fract_div_mul_self_mem_Ico {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] (a b : k) (ha : 0 < a) :
        fract (b / a) * a ∈ Set.Ico 0 a
        source
        theorem Int.fract_div_mul_self_add_zsmul_eq {k : Type u_4} [Field k] [LinearOrder k] [FloorRing k] (a b : k) (ha : a ≠ 0) :
        fract (b / a) * a + ⌊b / a⌋ • a = b
        source
        theorem Int.sub_floor_div_mul_nonneg {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) :
        0 ≤ a - ↑⌊a / b⌋ * b
        source
        theorem Int.sub_floor_div_mul_lt {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) :
        a - ↑⌊a / b⌋ * b < b
        source
        theorem Int.fract_div_natCast_eq_div_natCast_mod {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {m n : ℕ} :
        fract (↑m / ↑n) = ↑(m % n) / ↑n
        source
        theorem Int.fract_div_intCast_eq_div_intCast_mod {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {m : ℤ} {n : ℕ} :
        fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

        Ceil #

        source
        @[deprecated Int.lt_ceil (since := "2025-12-26")]
        theorem Int.add_one_le_ceil_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
        z + 1 ≤ ⌈a⌉ ↔ ↑z < a
        source
        @[simp]
        theorem Int.one_le_ceil_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        1 ≤ ⌈a⌉ ↔ 0 < a
        source
        theorem Int.ceil_le_floor_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) :
        ⌈a⌉ ≤ ⌊a⌋ + 1
        source
        theorem Int.ceil_mono {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] :
        Monotone ceil
        source
        theorem Int.ceil_le_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} (hab : a ≤ b) :
        ⌈a⌉ ≤ ⌈b⌉
        source
        theorem Int.ceil_nonneg_of_neg_one_lt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : -1 < a) :
        0 ≤ ⌈a⌉
        source
        theorem Int.ceil_eq_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
        ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z
        source
        @[simp]
        theorem Int.ceil_eq_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        ⌈a⌉ = 0 ↔ a ∈ Set.Ioc (-1) 0
        source
        theorem Int.ceil_eq_on_Ioc {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (z : ℤ) (a : R) :
        a ∈ Set.Ioc (↑z - 1) ↑z → ⌈a⌉ = z
        source
        @[simp]
        theorem Int.preimage_ceil_singleton {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (m : ℤ) :
        ceil ⁻¹' {m} = Set.Ioc (↑m - 1) ↑m
        source
        theorem Int.floor_neg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsOrderedRing R] :
        ⌊-a⌋ = -⌈a⌉
        source
        theorem Int.ceil_neg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsOrderedRing R] :
        ⌈-a⌉ = -⌊a⌋
        source
        @[simp]
        theorem Int.ceil_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (z : ℤ) :
        ⌈↑z⌉ = z
        source
        @[simp]
        theorem Int.ceil_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) :
        ⌈↑n⌉ = ↑n
        source
        @[simp]
        theorem Int.ceil_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) [n.AtLeastTwo] :
        ⌈OfNat.ofNat n⌉ = OfNat.ofNat n
        source
        @[simp]
        theorem Int.ceil_add_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ) :
        ⌈a + ↑z⌉ = ⌈a⌉ + z
        source
        @[simp]
        theorem Int.ceil_intCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (z : ℤ) (a : R) :
        ⌈↑z + a⌉ = z + ⌈a⌉
        source
        @[simp]
        theorem Int.ceil_add_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) :
        ⌈a + ↑n⌉ = ⌈a⌉ + ↑n
        source
        @[simp]
        theorem Int.ceil_natCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) (a : R) :
        ⌈↑n + a⌉ = ↑n + ⌈a⌉
        source
        @[simp]
        theorem Int.ceil_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌈a + 1⌉ = ⌈a⌉ + 1
        source
        @[simp]
        theorem Int.ceil_one_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌈1 + a⌉ = 1 + ⌈a⌉
        source
        @[simp]
        theorem Int.ceil_add_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] :
        ⌈a + OfNat.ofNat n⌉ = ⌈a⌉ + OfNat.ofNat n
        source
        @[simp]
        theorem Int.ceil_ofNat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (n : ℕ) [n.AtLeastTwo] (a : R) :
        ⌈OfNat.ofNat n + a⌉ = OfNat.ofNat n + ⌈a⌉
        source
        @[simp]
        theorem Int.ceil_sub_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ) :
        ⌈a - ↑z⌉ = ⌈a⌉ - z
        source
        @[simp]
        theorem Int.ceil_sub_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) :
        ⌈a - ↑n⌉ = ⌈a⌉ - ↑n
        source
        @[simp]
        theorem Int.ceil_sub_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌈a - 1⌉ = ⌈a⌉ - 1
        source
        @[simp]
        theorem Int.ceil_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] :
        ⌈a - OfNat.ofNat n⌉ = ⌈a⌉ - OfNat.ofNat n
        source
        theorem Int.ceil_lt_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ↑⌈a⌉ < a + 1
        source
        theorem Int.ceil_add_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a b : R) :
        ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉
        source
        theorem Int.ceil_add_ceil_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a b : R) :
        ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1
        source
        @[simp]
        theorem Int.ceil_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] :
        ⌈0⌉ = 0
        source
        @[simp]
        theorem Int.ceil_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] :
        ⌈1⌉ = 1
        source
        theorem Int.ceil_eq_on_Ioc' {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (z : ℤ) (a : R) :
        a ∈ Set.Ioc (↑z - 1) ↑z → ↑⌈a⌉ = ↑z
        source
        theorem Int.ceil_eq_self_iff_mem {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ↑⌈a⌉ = a ↔ a ∈ Set.range Int.cast
        source
        theorem Int.floor_le_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌊a⌋ ≤ ⌈a⌉
        source
        theorem Int.floor_lt_ceil_of_lt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] {a b : R} (h : a < b) :
        ⌊a⌋ < ⌈b⌉
        source
        theorem Int.ceil_eq_floor_add_one_iff_notMem {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast
        source
        theorem Int.fract_eq_zero_or_add_one_sub_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsOrderedRing R] (a : R) :
        fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
        source
        theorem Int.ceil_eq_add_one_sub_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsOrderedRing R] (ha : fract a ≠ 0) :
        ↑⌈a⌉ = a + 1 - fract a
        source
        theorem Int.ceil_sub_self_eq {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsOrderedRing R] (ha : fract a ≠ 0) :
        ↑⌈a⌉ - a = 1 - fract a
        source
        theorem Int.mul_lt_floor {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k} (hb₀ : 0 < b) (hb : b < 1) (hba : ↑⌈b / (1 - b)⌉ ≤ a) :
        b * a < ↑⌊a⌋
        source
        theorem Int.ceil_div_ceil_inv_sub_one {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 1 ≤ a) :
        ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉
        source
        theorem Int.ceil_lt_mul {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b < a) :
        ↑⌈a⌉ < b * a
        source
        theorem Int.ceil_le_mul {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ a) :
        ↑⌈a⌉ ≤ b * a
        source
        theorem Int.div_two_lt_floor {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 1 ≤ a) :
        a / 2 < ↑⌊a⌋
        source
        theorem Int.ceil_lt_two_mul {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 2⁻¹ < a) :
        ↑⌈a⌉ < 2 * a
        source
        theorem Int.ceil_le_two_mul {k : Type u_4} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a : k} (ha : 2⁻¹ ≤ a) :
        ↑⌈a⌉ ≤ 2 * a

        Intervals #

        source
        @[simp]
        theorem Int.preimage_Ioo {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} :
        Int.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉
        source
        @[simp]
        theorem Int.preimage_Ico {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} :
        Int.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉
        source
        @[simp]
        theorem Int.preimage_Ioc {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} :
        Int.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋
        source
        @[simp]
        theorem Int.preimage_Icc {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} :
        Int.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋
        source
        @[simp]
        theorem Int.preimage_Ioi {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        Int.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋
        source
        @[simp]
        theorem Int.preimage_Ici {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        Int.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉
        source
        @[simp]
        theorem Int.preimage_Iio {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        Int.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉
        source
        @[simp]
        theorem Int.preimage_Iic {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} :
        Int.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋
        source
        theorem Int.floor_congr {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] {a : R} {b : S} (h : ∀ (n : ℤ), ↑n ≤ a ↔ ↑n ≤ b) :
        ⌊a⌋ = ⌊b⌋
        source
        theorem Int.ceil_congr {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] {a : R} {b : S} (h : ∀ (n : ℤ), a ≤ ↑n ↔ b ≤ ↑n) :
        ⌈a⌉ = ⌈b⌉
        source
        theorem Int.map_floor {F : Type u_1} {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : StrictMono ⇑f) (a : R) :
        ⌊f a⌋ = ⌊a⌋
        source
        theorem Int.map_ceil {F : Type u_1} {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : StrictMono ⇑f) (a : R) :
        ⌈f a⌉ = ⌈a⌉
        source
        theorem Int.map_fract {F : Type u_1} {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : StrictMono ⇑f) (a : R) :
        fract (f a) = f (fract a)
        source
        theorem Nat.ceil_lt_add_one_of_gt_neg_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a : R} (ha : -1 < a) :
        ↑⌈a⌉₊ < a + 1

        a variant of Nat.ceil_lt_add_one with its condition 0 ≤ a generalized to -1 < a

        A floor ring as a floor semiring #

        source
        theorem Int.natCast_floor_eq_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : 0 ≤ a) :
        ↑⌊a⌋₊ = ⌊a⌋
        source
        theorem Int.natCast_ceil_eq_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : 0 ≤ a) :
        ↑⌈a⌉₊ = ⌈a⌉
        source
        theorem Int.natCast_ceil_eq_ceil_of_neg_one_lt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : -1 < a) :
        ↑⌈a⌉₊ = ⌈a⌉
        source
        theorem natCast_floor_eq_intCast_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : 0 ≤ a) :
        ↑⌊a⌋₊ = ↑⌊a⌋
        source
        theorem natCast_ceil_eq_intCast_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : 0 ≤ a) :
        ↑⌈a⌉₊ = ↑⌈a⌉
        source
        theorem natCast_ceil_eq_intCast_ceil_of_neg_one_lt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : -1 < a) :
        ↑⌈a⌉₊ = ↑⌈a⌉
        source
        theorem subsingleton_floorRing {R : Type u_4} [Ring R] [LinearOrder R] :
        Subsingleton (FloorRing R)

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