diff --git a/Mathlib/Algebra/Order/Round.lean b/Mathlib/Algebra/Order/Round.lean index b4cb18fd8672a..126741c7c3750 100644 --- a/Mathlib/Algebra/Order/Round.lean +++ b/Mathlib/Algebra/Order/Round.lean @@ -6,7 +6,6 @@ Authors: Mario Carneiro, Kevin Kappelmann import Mathlib.Algebra.Order.Floor import Mathlib.Algebra.Order.Interval.Set.Group - /-! # Rounding