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

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
@[simp]
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
@[deprecated Int.floor_add_intCast (since := "2025-04-01")]
theorem Int.floor_add_int {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) :
⌊a + ↑z⌋ = ⌊a⌋ + z

Alias of Int.floor_add_intCast.

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
@[deprecated Int.floor_intCast_add (since := "2025-04-01")]
theorem Int.floor_int_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) (a : R) :
⌊↑z + a⌋ = z + ⌊a⌋

Alias of Int.floor_intCast_add.

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
@[deprecated Int.floor_add_natCast (since := "2025-04-01")]
theorem Int.floor_add_nat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) :
⌊a + ↑n⌋ = ⌊a⌋ + ↑n

Alias of Int.floor_add_natCast.

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
@[deprecated Int.floor_natCast_add (since := "2025-04-01")]
theorem Int.floor_nat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) (a : R) :
⌊↑n + a⌋ = ↑n + ⌊a⌋

Alias of Int.floor_natCast_add.

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
@[deprecated Int.floor_sub_intCast (since := "2025-04-01")]
theorem Int.floor_sub_int {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) :
⌊a - ↑z⌋ = ⌊a⌋ - z

Alias of Int.floor_sub_intCast.

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
@[deprecated Int.floor_sub_natCast (since := "2025-04-01")]
theorem Int.floor_sub_nat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) :
⌊a - ↑n⌋ = ⌊a⌋ - ↑n

Alias of Int.floor_sub_natCast.

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

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
@[deprecated Int.fract_add_intCast (since := "2025-04-01")]
theorem Int.fract_add_int {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (m : ℤ) :
fract (a + ↑m) = fract a

Alias of Int.fract_add_intCast.

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
@[deprecated Int.fract_add_natCast (since := "2025-04-01")]
theorem Int.fract_add_nat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (m : ℕ) :
fract (a + ↑m) = fract a

Alias of Int.fract_add_natCast.

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
@[deprecated Int.fract_intCast_add (since := "2025-04-01")]
theorem Int.fract_int_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (m : ℤ) (a : R) :
fract (↑m + a) = fract a

Alias of Int.fract_intCast_add.

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
@[deprecated Int.fract_natCast_add (since := "2025-04-01")]
theorem Int.fract_nat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) (a : R) :
fract (↑n + a) = fract a

Alias of Int.fract_natCast_add.

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
@[deprecated Int.fract_sub_intCast (since := "2025-04-01")]
theorem Int.fract_sub_int {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (m : ℤ) :
fract (a - ↑m) = fract a

Alias of Int.fract_sub_intCast.

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
@[deprecated Int.fract_sub_natCast (since := "2025-04-01")]
theorem Int.fract_sub_nat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) :
fract (a - ↑n) = fract a

Alias of Int.fract_sub_natCast.

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_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
@[deprecated Int.fract_mul_natCast (since := "2025-04-01")]
theorem Int.fract_mul_nat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (b : ℕ) :
∃ (z : ℤ), fract a * ↑b - fract (a * ↑b) = ↑z

Alias of Int.fract_mul_natCast.

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
@[simp]
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.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
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
@[deprecated Int.ceil_add_intCast (since := "2025-04-01")]
theorem Int.ceil_add_int {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) :
⌈a + ↑z⌉ = ⌈a⌉ + z

Alias of Int.ceil_add_intCast.

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
@[deprecated Int.ceil_add_natCast (since := "2025-04-01")]
theorem Int.ceil_add_nat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) :
⌈a + ↑n⌉ = ⌈a⌉ + ↑n

Alias of Int.ceil_add_natCast.

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_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_sub_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) :
⌈a - ↑z⌉ = ⌈a⌉ - z
source
@[deprecated Int.ceil_sub_intCast (since := "2025-04-01")]
theorem Int.ceil_sub_int {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) :
⌈a - ↑z⌉ = ⌈a⌉ - z

Alias of Int.ceil_sub_intCast.

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
@[deprecated Int.ceil_sub_natCast (since := "2025-04-01")]
theorem Int.ceil_sub_nat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) :
⌈a - ↑n⌉ = ⌈a⌉ - ↑n

Alias of Int.ceil_sub_natCast.

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
@[deprecated Int.ceil_eq_floor_add_one_iff_notMem (since := "2025-05-23")]
theorem Int.ceil_eq_floor_add_one_iff_not_mem {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) :
⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast

Alias of Int.ceil_eq_floor_add_one_iff_notMem.

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)

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.