Theorems · Definition · number theory
round
{α : Type u_2} → [inst : Ring α] → [inst_1 : LinearOrder α] → [FloorRing α] → α → ℤround x rounds x to the nearest integer, breaking ties towards positive infinity.
round (0.5 : ℚ) = 1.
- Defined in
- Mathlib.Algebra.Order.Round
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
- Assumes
- RingLinearOrderFloorRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by50
Results whose statement or proof uses this declaration.
- round_eqstatement and proof · cited by 8
- AddCircle.norm_eqstatement and proof · cited by 6
- round_add_intCaststatement and proof · cited by 4
- Rat.round_caststatement and proof · cited by 3
- abs_sub_round_eq_minstatement · cited by 3
- round_lestatement · cited by 3
- abs_sub_roundstatement · cited by 2
- GaussianInt.div_defstatement and proof · cited by 2
- round_add_natCaststatement and proof · cited by 2
- round_eq_divstatement and proof · cited by 2
- round_intCaststatement · cited by 2
- round_natCaststatement · cited by 2