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 toa
. It rounds halves towards infinity.
Tags #
rounding
Round #
@[simp]
@[simp]
@[simp]
@[deprecated round_add_intCast (since := "2025-03-23")]
Alias of round_add_intCast
.
@[simp]
@[deprecated round_sub_intCast (since := "2025-03-23")]
Alias of round_sub_intCast
.
@[simp]
@[deprecated round_add_natCast (since := "2025-03-23")]
Alias of round_add_natCast
.
@[simp]
theorem
round_add_ofNat
{α : Type u_2}
[LinearOrderedRing α]
[FloorRing α]
(x : α)
(n : ℕ)
[n.AtLeastTwo]
:
@[deprecated round_sub_natCast (since := "2025-03-23")]
Alias of round_sub_natCast
.
@[simp]
theorem
round_sub_ofNat
{α : Type u_2}
[LinearOrderedRing α]
[FloorRing α]
(x : α)
(n : ℕ)
[n.AtLeastTwo]
:
@[deprecated round_intCast_add (since := "2025-03-23")]
Alias of round_intCast_add
.
@[deprecated round_natCast_add (since := "2025-03-23")]
Alias of round_natCast_add
.
@[simp]
theorem
round_ofNat_add
{α : Type u_2}
[LinearOrderedRing α]
[FloorRing α]
(n : ℕ)
[n.AtLeastTwo]
(x : α)
:
@[simp]
@[simp]
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 : α)
: