# mathlib3documentation

algebra.order.floor

# Floor and ceil #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Summary #

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

## Main Definitions #

• `floor_semiring`: An ordered semiring with natural-valued floor and ceil.

• `nat.floor a`: Greatest natural `n` such that `n ≤ a`. Equal to `0` if `a < 0`.

• `nat.ceil a`: Least natural `n` such that `a ≤ n`.

• `floor_ring`: A linearly ordered ring with integer-valued floor and ceil.

• `int.floor a`: Greatest integer `z` such that `z ≤ a`.

• `int.ceil a`: Least integer `z` such that `a ≤ z`.

• `int.fract a`: Fractional part of `a`, defined as `a - floor a`.

• `round a`: Nearest integer to `a`. It rounds halves towards infinity.

## Notations #

• `⌊a⌋₊` is `nat.floor a`.
• `⌈a⌉₊` is `nat.ceil a`.
• `⌊a⌋` is `int.floor a`.
• `⌈a⌉` is `int.ceil a`.

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

## TODO #

`linear_ordered_ring`/`linear_ordered_semiring` can be relaxed to `order_ring`/`order_semiring` in many lemmas.

## Tags #

rounding, floor, ceil

### Floor semiring #

@[class]
structure floor_semiring (α : Type u_4)  :
Type u_4

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

Instances of this typeclass
Instances of other typeclasses for `floor_semiring`
• floor_semiring.has_sizeof_inst
@[protected, instance]
Equations
def nat.floor {α : Type u_2}  :
α

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

Equations
def nat.ceil {α : Type u_2}  :
α

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

Equations
@[simp]
theorem nat.floor_nat  :
@[simp]
theorem nat.ceil_nat  :
theorem nat.le_floor_iff {α : Type u_2} {a : α} {n : } (ha : 0 a) :
theorem nat.le_floor {α : Type u_2} {a : α} {n : } (h : n a) :
theorem nat.floor_lt {α : Type u_2} {a : α} {n : } (ha : 0 a) :
theorem nat.floor_lt_one {α : Type u_2} {a : α} (ha : 0 a) :
a⌋₊ < 1 a < 1
theorem nat.lt_of_floor_lt {α : Type u_2} {a : α} {n : } (h : a⌋₊ < n) :
a < n
theorem nat.lt_one_of_floor_lt_one {α : Type u_2} {a : α} (h : a⌋₊ < 1) :
a < 1
theorem nat.floor_le {α : Type u_2} {a : α} (ha : 0 a) :
theorem nat.lt_succ_floor {α : Type u_2} (a : α) :
theorem nat.lt_floor_add_one {α : Type u_2} (a : α) :
@[simp]
theorem nat.floor_coe {α : Type u_2} (n : ) :
@[simp]
theorem nat.floor_zero {α : Type u_2}  :
@[simp]
theorem nat.floor_one {α : Type u_2}  :
theorem nat.floor_of_nonpos {α : Type u_2} {a : α} (ha : a 0) :
theorem nat.floor_mono {α : Type u_2}  :
theorem nat.le_floor_iff' {α : Type u_2} {a : α} {n : } (hn : n 0) :
@[simp]
theorem nat.one_le_floor_iff {α : Type u_2} (x : α) :
theorem nat.floor_lt' {α : Type u_2} {a : α} {n : } (hn : n 0) :
theorem nat.floor_pos {α : Type u_2} {a : α} :
theorem nat.pos_of_floor_pos {α : Type u_2} {a : α} (h : 0 < a⌋₊) :
0 < a
theorem nat.lt_of_lt_floor {α : Type u_2} {a : α} {n : } (h : n < a⌋₊) :
n < a
theorem nat.floor_le_of_le {α : Type u_2} {a : α} {n : } (h : a n) :
theorem nat.floor_le_one_of_le_one {α : Type u_2} {a : α} (h : a 1) :
@[simp]
theorem nat.floor_eq_zero {α : Type u_2} {a : α} :
a⌋₊ = 0 a < 1
theorem nat.floor_eq_iff {α : Type u_2} {a : α} {n : } (ha : 0 a) :
a⌋₊ = n n a a < n + 1
theorem nat.floor_eq_iff' {α : Type u_2} {a : α} {n : } (hn : n 0) :
a⌋₊ = n n a a < n + 1
theorem nat.floor_eq_on_Ico {α : Type u_2} (n : ) (a : α) (H : a (n + 1)) :
theorem nat.floor_eq_on_Ico' {α : Type u_2} (n : ) (a : α) (H : a (n + 1)) :
@[simp]
theorem nat.preimage_floor_zero {α : Type u_2}  :
theorem nat.preimage_floor_of_ne_zero {α : Type u_2} {n : } (hn : n 0) :

#### Ceil #

theorem nat.gc_ceil_coe {α : Type u_2}  :
@[simp]
theorem nat.ceil_le {α : Type u_2} {a : α} {n : } :
theorem nat.lt_ceil {α : Type u_2} {a : α} {n : } :
@[simp]
theorem nat.add_one_le_ceil_iff {α : Type u_2} {a : α} {n : } :
@[simp]
theorem nat.one_le_ceil_iff {α : Type u_2} {a : α} :
theorem nat.ceil_le_floor_add_one {α : Type u_2} (a : α) :
theorem nat.le_ceil {α : Type u_2} (a : α) :
@[simp]
theorem nat.ceil_int_cast {α : Type u_1} (z : ) :
@[simp]
theorem nat.ceil_nat_cast {α : Type u_2} (n : ) :
theorem nat.ceil_mono {α : Type u_2}  :
@[simp]
theorem nat.ceil_zero {α : Type u_2}  :
@[simp]
theorem nat.ceil_one {α : Type u_2}  :
@[simp]
theorem nat.ceil_eq_zero {α : Type u_2} {a : α} :
@[simp]
theorem nat.ceil_pos {α : Type u_2} {a : α} :
0 < a⌉₊ 0 < a
theorem nat.lt_of_ceil_lt {α : Type u_2} {a : α} {n : } (h : a⌉₊ < n) :
a < n
theorem nat.le_of_ceil_le {α : Type u_2} {a : α} {n : } (h : a⌉₊ n) :
a n
theorem nat.floor_le_ceil {α : Type u_2} (a : α) :
theorem nat.floor_lt_ceil_of_lt_of_pos {α : Type u_2} {a b : α} (h : a < b) (h' : 0 < b) :
theorem nat.ceil_eq_iff {α : Type u_2} {a : α} {n : } (hn : n 0) :
a⌉₊ = n (n - 1) < a a n
@[simp]
theorem nat.preimage_ceil_zero {α : Type u_2}  :
theorem nat.preimage_ceil_of_ne_zero {α : Type u_2} {n : } (hn : n 0) :

#### Intervals #

@[simp]
theorem nat.preimage_Ioo {α : Type u_2} {a b : α} (ha : 0 a) :
@[simp]
theorem nat.preimage_Ico {α : Type u_2} {a b : α} :
@[simp]
theorem nat.preimage_Ioc {α : Type u_2} {a b : α} (ha : 0 a) (hb : 0 b) :
@[simp]
theorem nat.preimage_Icc {α : Type u_2} {a b : α} (hb : 0 b) :
@[simp]
theorem nat.preimage_Ioi {α : Type u_2} {a : α} (ha : 0 a) :
=
@[simp]
theorem nat.preimage_Ici {α : Type u_2} {a : α} :
=
@[simp]
theorem nat.preimage_Iio {α : Type u_2} {a : α} :
=
@[simp]
theorem nat.preimage_Iic {α : Type u_2} {a : α} (ha : 0 a) :
=
theorem nat.floor_add_nat {α : Type u_2} {a : α} (ha : 0 a) (n : ) :
theorem nat.floor_add_one {α : Type u_2} {a : α} (ha : 0 a) :
theorem nat.floor_sub_nat {α : Type u_2} [has_sub α] (a : α) (n : ) :
theorem nat.ceil_add_nat {α : Type u_2} {a : α} (ha : 0 a) (n : ) :
theorem nat.ceil_add_one {α : Type u_2} {a : α} (ha : 0 a) :
theorem nat.ceil_lt_add_one {α : Type u_2} {a : α} (ha : 0 a) :
theorem nat.ceil_add_le {α : Type u_2} (a b : α) :
theorem nat.sub_one_lt_floor {α : Type u_2} (a : α) :
theorem nat.floor_div_nat {α : Type u_2} (a : α) (n : ) :
theorem nat.floor_div_eq_div {α : Type u_2} (m n : ) :

Natural division is the floor of field division.

theorem subsingleton_floor_semiring {α : Type u_1}  :

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

### Floor rings #

@[class]
structure floor_ring (α : Type u_4)  :
Type u_4
• floor : α
• ceil : α
• gc_coe_floor :
• gc_ceil_coe :

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

Instances of this typeclass
Instances of other typeclasses for `floor_ring`
• floor_ring.has_sizeof_inst
@[protected, instance]
Equations
def floor_ring.of_floor (α : Type u_1) (floor : α ) (gc_coe_floor : floor) :

A `floor_ring` constructor from the `floor` function alone.

Equations
def floor_ring.of_ceil (α : Type u_1) (ceil : α ) (gc_ceil_coe : coe) :

A `floor_ring` constructor from the `ceil` function alone.

Equations
def int.floor {α : Type u_2} [floor_ring α] :
α

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

Equations
def int.ceil {α : Type u_2} [floor_ring α] :
α

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

Equations
def int.fract {α : Type u_2} [floor_ring α] (a : α) :
α

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

Equations
@[simp]
theorem int.floor_int  :
@[simp]
theorem int.ceil_int  :
@[simp]
theorem int.fract_int  :
@[simp]
@[simp]

#### Floor #

theorem int.gc_coe_floor {α : Type u_2} [floor_ring α] :
theorem int.le_floor {α : Type u_2} [floor_ring α] {z : } {a : α} :
theorem int.floor_lt {α : Type u_2} [floor_ring α] {z : } {a : α} :
a < z a < z
theorem int.floor_le {α : Type u_2} [floor_ring α] (a : α) :
theorem int.floor_nonneg {α : Type u_2} [floor_ring α] {a : α} :
0 a 0 a
@[simp]
theorem int.floor_le_sub_one_iff {α : Type u_2} [floor_ring α] {z : } {a : α} :
a z - 1 a < z
@[simp]
theorem int.floor_le_neg_one_iff {α : Type u_2} [floor_ring α] {a : α} :
a -1 a < 0
theorem int.floor_nonpos {α : Type u_2} [floor_ring α] {a : α} (ha : a 0) :
theorem int.lt_succ_floor {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.lt_floor_add_one {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.sub_one_lt_floor {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.floor_int_cast {α : Type u_2} [floor_ring α] (z : ) :
@[simp]
theorem int.floor_nat_cast {α : Type u_2} [floor_ring α] (n : ) :
@[simp]
theorem int.floor_zero {α : Type u_2} [floor_ring α] :
@[simp]
theorem int.floor_one {α : Type u_2} [floor_ring α] :
theorem int.floor_mono {α : Type u_2} [floor_ring α] :
theorem int.floor_pos {α : Type u_2} [floor_ring α] {a : α} :
0 < a 1 a
@[simp]
theorem int.floor_add_int {α : Type u_2} [floor_ring α] (a : α) (z : ) :
theorem int.floor_add_one {α : Type u_2} [floor_ring α] (a : α) :
a + 1 = a + 1
theorem int.le_floor_add {α : Type u_2} [floor_ring α] (a b : α) :
theorem int.le_floor_add_floor {α : Type u_2} [floor_ring α] (a b : α) :
@[simp]
theorem int.floor_int_add {α : Type u_2} [floor_ring α] (z : ) (a : α) :
@[simp]
theorem int.floor_add_nat {α : Type u_2} [floor_ring α] (a : α) (n : ) :
@[simp]
theorem int.floor_nat_add {α : Type u_2} [floor_ring α] (n : ) (a : α) :
@[simp]
theorem int.floor_sub_int {α : Type u_2} [floor_ring α] (a : α) (z : ) :
@[simp]
theorem int.floor_sub_nat {α : Type u_2} [floor_ring α] (a : α) (n : ) :
theorem int.abs_sub_lt_one_of_floor_eq_floor {α : Type u_1} [floor_ring α] {a b : α} (h : a = b) :
|a - b| < 1
theorem int.floor_eq_iff {α : Type u_2} [floor_ring α] {z : } {a : α} :
a = z z a a < z + 1
@[simp]
theorem int.floor_eq_zero_iff {α : Type u_2} [floor_ring α] {a : α} :
a = 0 a 1
theorem int.floor_eq_on_Ico {α : Type u_2} [floor_ring α] (n : ) (a : α) (H : a (n + 1)) :
theorem int.floor_eq_on_Ico' {α : Type u_2} [floor_ring α] (n : ) (a : α) (H : a (n + 1)) :
@[simp]
theorem int.preimage_floor_singleton {α : Type u_2} [floor_ring α] (m : ) :

#### Fractional part #

@[simp]
theorem int.self_sub_floor {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.floor_add_fract {α : Type u_2} [floor_ring α] (a : α) :
= a
@[simp]
theorem int.fract_add_floor {α : Type u_2} [floor_ring α] (a : α) :
= a
@[simp]
theorem int.fract_add_int {α : Type u_2} [floor_ring α] (a : α) (m : ) :
@[simp]
theorem int.fract_add_nat {α : Type u_2} [floor_ring α] (a : α) (m : ) :
@[simp]
theorem int.fract_sub_int {α : Type u_2} [floor_ring α] (a : α) (m : ) :
@[simp]
theorem int.fract_int_add {α : Type u_2} [floor_ring α] (m : ) (a : α) :
@[simp]
theorem int.fract_sub_nat {α : Type u_2} [floor_ring α] (a : α) (n : ) :
@[simp]
theorem int.fract_int_nat {α : Type u_2} [floor_ring α] (n : ) (a : α) :
theorem int.fract_add_le {α : Type u_2} [floor_ring α] (a b : α) :
int.fract (a + b)
theorem int.fract_add_fract_le {α : Type u_2} [floor_ring α] (a b : α) :
int.fract (a + b) + 1
@[simp]
theorem int.self_sub_fract {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.fract_sub_self {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.fract_nonneg {α : Type u_2} [floor_ring α] (a : α) :
0
theorem int.fract_pos {α : Type u_2} [floor_ring α] {a : α} :

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

theorem int.fract_lt_one {α : Type u_2} [floor_ring α] (a : α) :
< 1
@[simp]
theorem int.fract_zero {α : Type u_2} [floor_ring α] :
= 0
@[simp]
theorem int.fract_one {α : Type u_2} [floor_ring α] :
= 0
theorem int.abs_fract {α : Type u_2} [floor_ring α] {a : α} :
@[simp]
theorem int.abs_one_sub_fract {α : Type u_2} [floor_ring α] {a : α} :
|1 - | = 1 -
@[simp]
theorem int.fract_int_cast {α : Type u_2} [floor_ring α] (z : ) :
= 0
@[simp]
theorem int.fract_nat_cast {α : Type u_2} [floor_ring α] (n : ) :
= 0
@[simp]
theorem int.fract_floor {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.floor_fract {α : Type u_2} [floor_ring α] (a : α) :
= 0
theorem int.fract_eq_iff {α : Type u_2} [floor_ring α] {a b : α} :
= b 0 b b < 1 (z : ), a - b = z
theorem int.fract_eq_fract {α : Type u_2} [floor_ring α] {a b : α} :
(z : ), a - b = z
@[simp]
theorem int.fract_eq_self {α : Type u_2} [floor_ring α] {a : α} :
= a 0 a a < 1
@[simp]
theorem int.fract_fract {α : Type u_2} [floor_ring α] (a : α) :
=
theorem int.fract_add {α : Type u_2} [floor_ring α] (a b : α) :
(z : ), int.fract (a + b) - - = z
theorem int.fract_neg {α : Type u_2} [floor_ring α] {x : α} (hx : 0) :
int.fract (-x) = 1 -
@[simp]
theorem int.fract_neg_eq_zero {α : Type u_2} [floor_ring α] {x : α} :
int.fract (-x) = 0 = 0
theorem int.fract_mul_nat {α : Type u_2} [floor_ring α] (a : α) (b : ) :
(z : ), * b - int.fract (a * b) = z
theorem int.preimage_fract {α : Type u_2} [floor_ring α] (s : set α) :
= (m : ), (λ (x : α), x - m) ⁻¹' (s 1)
theorem int.image_fract {α : Type u_2} [floor_ring α] (s : set α) :
= (m : ), (λ (x : α), x - m) '' s 1
theorem int.fract_div_mul_self_mem_Ico {k : Type u_4} [floor_ring k] (a b : k) (ha : 0 < a) :
int.fract (b / a) * a a
theorem int.fract_div_mul_self_add_zsmul_eq {k : Type u_4} [floor_ring k] (a b : k) (ha : a 0) :
int.fract (b / a) * a + b / a a = b
theorem int.sub_floor_div_mul_nonneg {k : Type u_4} [floor_ring k] {b : k} (a : k) (hb : 0 < b) :
0 a - a / b * b
theorem int.sub_floor_div_mul_lt {k : Type u_4} [floor_ring k] {b : k} (a : k) (hb : 0 < b) :
a - a / b * b < b

#### Ceil #

theorem int.gc_ceil_coe {α : Type u_2} [floor_ring α] :
theorem int.ceil_le {α : Type u_2} [floor_ring α] {z : } {a : α} :
theorem int.floor_neg {α : Type u_2} [floor_ring α] {a : α} :
theorem int.ceil_neg {α : Type u_2} [floor_ring α] {a : α} :
theorem int.lt_ceil {α : Type u_2} [floor_ring α] {z : } {a : α} :
z < a z < a
@[simp]
theorem int.add_one_le_ceil_iff {α : Type u_2} [floor_ring α] {z : } {a : α} :
z + 1 a z < a
@[simp]
theorem int.one_le_ceil_iff {α : Type u_2} [floor_ring α] {a : α} :
1 a 0 < a
theorem int.ceil_le_floor_add_one {α : Type u_2} [floor_ring α] (a : α) :
theorem int.le_ceil {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem int.ceil_int_cast {α : Type u_2} [floor_ring α] (z : ) :
@[simp]
theorem int.ceil_nat_cast {α : Type u_2} [floor_ring α] (n : ) :
theorem int.ceil_mono {α : Type u_2} [floor_ring α] :
@[simp]
theorem int.ceil_add_int {α : Type u_2} [floor_ring α] (a : α) (z : ) :
@[simp]
theorem int.ceil_add_nat {α : Type u_2} [floor_ring α] (a : α) (n : ) :
@[simp]
theorem int.ceil_add_one {α : Type u_2} [floor_ring α] (a : α) :
a + 1 = a + 1
@[simp]
theorem int.ceil_sub_int {α : Type u_2} [floor_ring α] (a : α) (z : ) :
@[simp]
theorem int.ceil_sub_nat {α : Type u_2} [floor_ring α] (a : α) (n : ) :
@[simp]
theorem int.ceil_sub_one {α : Type u_2} [floor_ring α] (a : α) :
a - 1 = a - 1
theorem int.ceil_lt_add_one {α : Type u_2} [floor_ring α] (a : α) :
theorem int.ceil_add_le {α : Type u_2} [floor_ring α] (a b : α) :
theorem int.ceil_add_ceil_le {α : Type u_2} [floor_ring α] (a b : α) :
@[simp]
theorem int.ceil_pos {α : Type u_2} [floor_ring α] {a : α} :
0 < a 0 < a
@[simp]
theorem int.ceil_zero {α : Type u_2} [floor_ring α] :
@[simp]
theorem int.ceil_one {α : Type u_2} [floor_ring α] :
theorem int.ceil_nonneg {α : Type u_2} [floor_ring α] {a : α} (ha : 0 a) :
theorem int.ceil_eq_iff {α : Type u_2} [floor_ring α] {z : } {a : α} :
a = z z - 1 < a a z
@[simp]
theorem int.ceil_eq_zero_iff {α : Type u_2} [floor_ring α] {a : α} :
a = 0 a set.Ioc (-1) 0
theorem int.ceil_eq_on_Ioc {α : Type u_2} [floor_ring α] (z : ) (a : α) (H : a set.Ioc (z - 1) z) :
theorem int.ceil_eq_on_Ioc' {α : Type u_2} [floor_ring α] (z : ) (a : α) (H : a set.Ioc (z - 1) z) :
theorem int.floor_le_ceil {α : Type u_2} [floor_ring α] (a : α) :
theorem int.floor_lt_ceil_of_lt {α : Type u_2} [floor_ring α] {a b : α} (h : a < b) :
@[simp]
theorem int.preimage_ceil_singleton {α : Type u_2} [floor_ring α] (m : ) :
theorem int.fract_eq_zero_or_add_one_sub_ceil {α : Type u_2} [floor_ring α] (a : α) :
= 0 = a + 1 - a
theorem int.ceil_eq_add_one_sub_fract {α : Type u_2} [floor_ring α] {a : α} (ha : 0) :
a = a + 1 -
theorem int.ceil_sub_self_eq {α : Type u_2} [floor_ring α] {a : α} (ha : 0) :
a - a = 1 -

#### Intervals #

@[simp]
theorem int.preimage_Ioo {α : Type u_2} [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Ico {α : Type u_2} [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Ioc {α : Type u_2} [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Icc {α : Type u_2} [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Ioi {α : Type u_2} [floor_ring α] {a : α} :
=
@[simp]
theorem int.preimage_Ici {α : Type u_2} [floor_ring α] {a : α} :
=
@[simp]
theorem int.preimage_Iio {α : Type u_2} [floor_ring α] {a : α} :
=
@[simp]
theorem int.preimage_Iic {α : Type u_2} [floor_ring α] {a : α} :
=

### Round #

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

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

Equations
@[simp]
theorem round_zero {α : Type u_2} [floor_ring α] :
= 0
@[simp]
theorem round_one {α : Type u_2} [floor_ring α] :
= 1
@[simp]
theorem round_nat_cast {α : Type u_2} [floor_ring α] (n : ) :
= n
@[simp]
theorem round_int_cast {α : Type u_2} [floor_ring α] (n : ) :
= n
@[simp]
theorem round_add_int {α : Type u_2} [floor_ring α] (x : α) (y : ) :
round (x + y) = + y
@[simp]
theorem round_add_one {α : Type u_2} [floor_ring α] (a : α) :
round (a + 1) = + 1
@[simp]
theorem round_sub_int {α : Type u_2} [floor_ring α] (x : α) (y : ) :
round (x - y) = - y
@[simp]
theorem round_sub_one {α : Type u_2} [floor_ring α] (a : α) :
round (a - 1) = - 1
@[simp]
theorem round_add_nat {α : Type u_2} [floor_ring α] (x : α) (y : ) :
round (x + y) = + y
@[simp]
theorem round_sub_nat {α : Type u_2} [floor_ring α] (x : α) (y : ) :
round (x - y) = - y
@[simp]
theorem round_int_add {α : Type u_2} [floor_ring α] (x : α) (y : ) :
round (y + x) = y +
@[simp]
theorem round_nat_add {α : Type u_2} [floor_ring α] (x : α) (y : ) :
round (y + x) = y +
theorem abs_sub_round_eq_min {α : Type u_2} [floor_ring α] (x : α) :
|x - (round x)| = (1 -
theorem round_le {α : Type u_2} [floor_ring α] (x : α) (z : ) :
theorem round_eq {α : Type u_2} [floor_ring α] (x : α) :
= x + 1 / 2
@[simp]
theorem round_two_inv {α : Type u_2} [floor_ring α] :
= 1
@[simp]
theorem round_neg_two_inv {α : Type u_2} [floor_ring α] :
@[simp]
theorem round_eq_zero_iff {α : Type u_2} [floor_ring α] {x : α} :
= 0 x set.Ico (-(1 / 2)) (1 / 2)
theorem abs_sub_round {α : Type u_2} [floor_ring α] (x : α) :
|x - (round x)| 1 / 2
theorem abs_sub_round_div_nat_cast_eq {α : Type u_2} [floor_ring α] {m n : } :
|m / n - (round (m / n))| = (linear_order.min (m % n) (n - m % n)) / n
theorem nat.floor_congr {α : Type u_2} {β : Type u_3} {a : α} {b : β} (h : (n : ), n a n b) :
theorem nat.ceil_congr {α : Type u_2} {β : Type u_3} {a : α} {b : β} (h : (n : ), a n b n) :
theorem nat.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) (hf : strict_mono f) (a : α) :
theorem nat.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) (hf : strict_mono f) (a : α) :
theorem int.floor_congr {α : Type u_2} {β : Type u_3} [floor_ring α] [floor_ring β] {a : α} {b : β} (h : (n : ), n a n b) :
theorem int.ceil_congr {α : Type u_2} {β : Type u_3} [floor_ring α] [floor_ring β] {a : α} {b : β} (h : (n : ), a n b n) :
theorem int.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [floor_ring α] [floor_ring β] [ β] (f : F) (hf : strict_mono f) (a : α) :
theorem int.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [floor_ring α] [floor_ring β] [ β] (f : F) (hf : strict_mono f) (a : α) :
theorem int.map_fract {F : Type u_1} {α : Type u_2} {β : Type u_3} [floor_ring α] [floor_ring β] [ β] (f : F) (hf : strict_mono f) (a : α) :
theorem int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [floor_ring α] [floor_ring β] [ β] (f : F) (hf : strict_mono f) (a : α) :
round (f a) =

#### A floor ring as a floor semiring #

@[protected, instance]
Equations
theorem int.floor_to_nat {α : Type u_2} [floor_ring α] (a : α) :
theorem int.ceil_to_nat {α : Type u_2} [floor_ring α] (a : α) :
@[simp]
theorem nat.floor_int  :
@[simp]
theorem nat.ceil_int  :
theorem nat.cast_floor_eq_int_floor {α : Type u_2} [floor_ring α] {a : α} (ha : 0 a) :
theorem nat.cast_floor_eq_cast_int_floor {α : Type u_2} [floor_ring α] {a : α} (ha : 0 a) :
theorem nat.cast_ceil_eq_int_ceil {α : Type u_2} [floor_ring α] {a : α} (ha : 0 a) :
theorem nat.cast_ceil_eq_cast_int_ceil {α : Type u_2} [floor_ring α] {a : α} (ha : 0 a) :
theorem subsingleton_floor_ring {α : Type u_1}  :

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

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

Extension for the `positivity` tactic: `ceil` and `int.ceil` are positive/nonnegative if their input is.