Skip to content

Commit 8f7035d

Browse files
committed
fix
1 parent e1835ce commit 8f7035d

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

Mathlib/Topology/Instances/Rat.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,8 @@ theorem uniformContinuous_add : UniformContinuous fun p : ℚ × ℚ => p.1 + p.
8282

8383
theorem uniformContinuous_neg : UniformContinuous (@Neg.neg ℚ _) :=
8484
Metric.uniformContinuous_iff.2 fun ε ε0 =>
85-
⟨_, ε0, fun _ _ h => by simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h⟩
85+
⟨_, ε0, fun _ _ h => by
86+
simpa only [_root_.abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h⟩
8687

8788
instance : IsUniformAddGroup ℚ :=
8889
IsUniformAddGroup.mk' Rat.uniformContinuous_add Rat.uniformContinuous_neg

0 commit comments

Comments
 (0)