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
    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.

      Equations
        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
            Instances For

              Floor rings #

              Floor #

              source
              theorem Int.floor_le_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
              ⌊a⌋ ≤ z ↔ a < ↑z + 1
              source
              theorem Int.lt_floor_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
              z < ⌊a⌋ ↔ ↑z + 1 ≤ a
              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] [IsStrictOrderedRing R] (a : R) :
              a - 1 < ↑⌊a⌋
              source
              @[simp]
              theorem Int.floor_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) :
              ⌊↑z⌋ = z
              source
              @[simp]
              theorem Int.floor_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) :
              ⌊↑n⌋ = ↑n
              source
              @[simp]
              theorem Int.floor_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] :
              ⌊0⌋ = 0
              source
              @[simp]
              theorem Int.floor_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] :
              ⌊1⌋ = 1
              source
              @[simp]
              theorem Int.floor_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              ⌊a + 1⌋ = ⌊a⌋ + 1
              source
              theorem Int.le_floor_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              ⌊a - 1⌋ = ⌊a⌋ - 1
              source
              @[simp]
              theorem Int.floor_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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} [CommRing 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} [CommRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              0 ≤ fract a
              source
              theorem Int.fract_pos {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              fract a < 1
              source
              @[simp]
              theorem Int.fract_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] :
              fract 0 = 0
              source
              @[simp]
              theorem Int.fract_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] :
              fract 1 = 0
              source
              theorem Int.abs_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing 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} [IsStrictOrderedRing R] :
              |1 - fract a| = 1 - fract a
              source
              @[simp]
              theorem Int.fract_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) :
              fract ↑z = 0
              source
              @[simp]
              theorem Int.fract_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) :
              fract ↑n = 0
              source
              @[simp]
              theorem Int.fract_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] :
              fract (OfNat.ofNat n) = 0
              source
              theorem Int.fract_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) :
              fract ↑⌊a⌋ = 0
              source
              @[simp]
              theorem Int.floor_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) :
              ⌊fract a⌋ = 0
              source
              theorem Int.fract_eq_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing k] [FloorRing k] {m : ℤ} {n : ℕ} :
              fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

              Ceil #

              source
              theorem Int.le_ceil_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
              z ≤ ⌈a⌉ ↔ ↑z - 1 < a
              source
              theorem Int.ceil_lt_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} :
              ⌈a⌉ < z ↔ a ≤ ↑z - 1
              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} [IsStrictOrderedRing R] :
              ⌊-a⌋ = -⌈a⌉
              source
              theorem Int.ceil_neg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] :
              ⌈-a⌉ = -⌊a⌋
              source
              @[simp]
              theorem Int.ceil_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) :
              ⌈↑z⌉ = z
              source
              @[simp]
              theorem Int.ceil_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) :
              ⌈↑n⌉ = ↑n
              source
              @[simp]
              theorem Int.ceil_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              ⌈a + 1⌉ = ⌈a⌉ + 1
              source
              @[simp]
              theorem Int.ceil_one_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) :
              ⌈1 + a⌉ = 1 + ⌈a⌉
              source
              @[simp]
              theorem Int.ceil_add_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              ⌈a - 1⌉ = ⌈a⌉ - 1
              source
              @[simp]
              theorem Int.ceil_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              ↑⌈a⌉ < a + 1
              source
              theorem Int.ceil_add_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] :
              ⌈0⌉ = 0
              source
              @[simp]
              theorem Int.ceil_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] :
              ⌈1⌉ = 1
              source
              theorem Int.ceil_eq_on_Ioc' {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing R] (a : R) :
              ⌊a⌋ ≤ ⌈a⌉
              source
              theorem Int.floor_lt_ceil_of_lt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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} [IsStrictOrderedRing 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} [IsStrictOrderedRing R] (ha : fract a ≠ 0) :
              ↑⌈a⌉ - a = 1 - fract a
              source
              theorem Int.mul_lt_floor {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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] [IsStrictOrderedRing 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.