Documentation

Mathlib.Algebra.Order.Round

Rounding #

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

Main Definitions #

Tags #

rounding

Round #

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

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

Equations
Instances For
    source
    @[simp]
    theorem round_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
    round 0 = 0
    source
    @[simp]
    theorem round_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] :
    round 1 = 1
    source
    @[simp]
    theorem round_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) :
    round ↑n = ↑n
    source
    @[simp]
    theorem round_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] :
    round (OfNat.ofNat n) = OfNat.ofNat n
    source
    @[simp]
    theorem round_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℤ) :
    round ↑n = n
    source
    @[simp]
    theorem round_add_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
    round (x + ↑y) = round x + y
    source
    @[deprecated round_add_intCast (since := "2025-03-23")]
    theorem round_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
    round (x + ↑y) = round x + y

    Alias of round_add_intCast.

    source
    @[simp]
    theorem round_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
    round (a + 1) = round a + 1
    source
    @[simp]
    theorem round_sub_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
    round (x - ↑y) = round x - y
    source
    @[deprecated round_sub_intCast (since := "2025-03-23")]
    theorem round_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
    round (x - ↑y) = round x - y

    Alias of round_sub_intCast.

    source
    @[simp]
    theorem round_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) :
    round (a - 1) = round a - 1
    source
    @[simp]
    theorem round_add_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
    round (x + ↑y) = round x + ↑y
    source
    @[deprecated round_add_natCast (since := "2025-03-23")]
    theorem round_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
    round (x + ↑y) = round x + ↑y

    Alias of round_add_natCast.

    source
    @[simp]
    theorem round_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (n : ℕ) [n.AtLeastTwo] :
    round (x + OfNat.ofNat n) = round x + OfNat.ofNat n
    source
    @[simp]
    theorem round_sub_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
    round (x - ↑y) = round x - ↑y
    source
    @[deprecated round_sub_natCast (since := "2025-03-23")]
    theorem round_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
    round (x - ↑y) = round x - ↑y

    Alias of round_sub_natCast.

    source
    @[simp]
    theorem round_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (n : ℕ) [n.AtLeastTwo] :
    round (x - OfNat.ofNat n) = round x - OfNat.ofNat n
    source
    @[simp]
    theorem round_intCast_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
    round (↑y + x) = y + round x
    source
    @[deprecated round_intCast_add (since := "2025-03-23")]
    theorem round_int_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) :
    round (↑y + x) = y + round x

    Alias of round_intCast_add.

    source
    @[simp]
    theorem round_natCast_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
    round (↑y + x) = ↑y + round x
    source
    @[deprecated round_natCast_add (since := "2025-03-23")]
    theorem round_nat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) :
    round (↑y + x) = ↑y + round x

    Alias of round_natCast_add.

    source
    @[simp]
    theorem round_ofNat_add {α : Type u_2} [LinearOrderedRing α] [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} [LinearOrderedRing α] [FloorRing α] (x : α) :
    |x - ↑(round x)| = Int.fract x ⊓ (1 - Int.fract x)
    source
    theorem round_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (z : ℤ) :
    |x - ↑(round x)| ≤ |x - ↑z|
    source
    theorem round_eq {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
    round x = ⌊x + 1 / 2⌋
    source
    @[simp]
    theorem round_two_inv {α : Type u_2} [LinearOrderedField α] [FloorRing α] :
    round 2⁻¹ = 1
    source
    @[simp]
    theorem round_neg_two_inv {α : Type u_2} [LinearOrderedField α] [FloorRing α] :
    round (-2⁻¹) = 0
    source
    @[simp]
    theorem round_eq_zero_iff {α : Type u_2} [LinearOrderedField α] [FloorRing α] {x : α} :
    round x = 0 ↔ x ∈ Set.Ico (-(1 / 2)) (1 / 2)
    source
    theorem abs_sub_round {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
    |x - ↑(round x)| ≤ 1 / 2
    source
    theorem abs_sub_round_div_natCast_eq {α : Type u_2} [LinearOrderedField α] [FloorRing α] {m n : ℕ} :
    |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(m % n ⊓ (n - m % n)) / ↑n
    source
    theorem sub_half_lt_round {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
    x - 1 / 2 < ↑(round x)
    source
    theorem round_le_add_half {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) :
    ↑(round x) ≤ x + 1 / 2
    source
    theorem Int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [LinearOrderedField β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) :
    round (f a) = round a