# Rounding #

This file defines the `round` function, which uses the `floor` or `ceil` function to round a number to the nearest integer.

## Main Definitions #

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

## Tags #

rounding

### Round #

source
def round {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (x : α) :
ℤ

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

Equations

- round x = if 2 * Int.fract x < 1 then ⌊x⌋ else ⌈x⌉

Instances For

source
@[simp]
theorem round_zero {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] :
round 0 = 0
source
@[simp]
theorem round_one {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] :
round 1 = 1
source
@[simp]
theorem round_natCast {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (n : ℕ) :
round ↑n = ↑n
source
@[simp]
theorem round_ofNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] :
round (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem round_intCast {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (n : ℤ) :
round ↑n = n
source
@[simp]
theorem round_add_intCast {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
round (x + ↑y) = round x + y
source
@[simp]
theorem round_add_one {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) :
round (a + 1) = round a + 1
source
@[simp]
theorem round_sub_intCast {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
round (x - ↑y) = round x - y
source
@[simp]
theorem round_sub_one {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) :
round (a - 1) = round a - 1
source
@[simp]
theorem round_add_natCast {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
round (x + ↑y) = round x + ↑y
source
@[simp]
theorem round_add_ofNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (n : ℕ) [n.AtLeastTwo] :
round (x + OfNat.ofNat n) = round x + OfNat.ofNat n
source
@[simp]
theorem round_sub_natCast {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
round (x - ↑y) = round x - ↑y
source
@[simp]
theorem round_sub_ofNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (n : ℕ) [n.AtLeastTwo] :
round (x - OfNat.ofNat n) = round x - OfNat.ofNat n
source
@[simp]
theorem round_intCast_add {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
round (↑y + x) = y + round x
source
@[simp]
theorem round_natCast_add {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
round (↑y + x) = ↑y + round x
source
@[simp]
theorem round_ofNat_add {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] (x : α) :
round (OfNat.ofNat n + x) = OfNat.ofNat n + round x
source
theorem abs_sub_round_eq_min {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) :
|x - ↑(round x)| = min (Int.fract x) (1 - Int.fract x)
source
theorem round_le {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (z : ℤ) :
|x - ↑(round x)| ≤ |x - ↑z|
source
theorem round_eq {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) :
round x = ⌊x + 1 / 2⌋
source
@[simp]
theorem round_two_inv {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] :
round 2⁻¹ = 1
source
@[simp]
theorem round_neg_two_inv {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] :
round (-2⁻¹) = 0
source
@[simp]
theorem round_eq_zero_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {x : α} :
round x = 0 ↔ x ∈ Set.Ico (-(1 / 2)) (1 / 2)
source
theorem abs_sub_round {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) :
|x - ↑(round x)| ≤ 1 / 2
source
theorem abs_sub_round_div_natCast_eq {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {m n : ℕ} :
|↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
source
theorem sub_half_lt_round {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) :
x - 1 / 2 < ↑(round x)
source
theorem round_le_add_half {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) :
↑(round x) ≤ x + 1 / 2
source
theorem Int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) :
round (f a) = round a