more

leanprover-community · Feb 2, 2025 · 3232203 · 3232203
1 parent b5cd6ce
commit 3232203
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -388,7 +388,7 @@ theorem inseparable_one_iff_norm {a : E} : Inseparable a 1 ↔ ‖a‖ = 0 := by
   rw [Metric.inseparable_iff, dist_one_right]
 
 @[to_additive]
-lemma dist_one_left (a : E) : dist (1 : E) a = ‖a‖ := by rw [dist_comm, dist_one_right]
+lemma dist_one_left (a : E) : dist 1 a = ‖a‖ := by rw [dist_comm, dist_one_right]
 
 @[to_additive (attr := simp)]
 lemma dist_one : dist (1 : E) = norm := funext dist_one_left