diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
index e3f93fb40be9b..f178ece3bbe0e 100644
--- a/Mathlib/Analysis/Normed/Group/Basic.lean
+++ b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -1096,12 +1096,12 @@ theorem comap_norm_nhds_one : comap norm (𝓝 0) = 𝓝 (1 : E) := by
 #align comap_norm_nhds_zero comap_norm_nhds_zero
 
 /-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real
-function `a` which tends to `0`, then `f` tends to `1`. In this pair of lemmas (`squeeze_one_norm'`
-and `squeeze_one_norm`), following a convention of similar lemmas in `Topology.MetricSpace.Basic`
-and `Topology.Algebra.Order`, the `'` version is phrased using "eventually" and the non-`'` version
-is phrased absolutely. -/
+function `a` which tends to `0`, then `f` tends to `1` (neutral element of `SeminormedGroup`).
+In this pair of lemmas (`squeeze_one_norm'` and `squeeze_one_norm`), following a convention of
+similar lemmas in `Topology.MetricSpace.Basic` and `Topology.Algebra.Order`, the `'` version is
+phrased using "eventually" and the non-`'` version is phrased absolutely. -/
 @[to_additive "Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a
-real function `a` which tends to `0`, then `f` tends to `1`. In this pair of lemmas
+real function `a` which tends to `0`, then `f` tends to `0`. In this pair of lemmas
 (`squeeze_zero_norm'` and `squeeze_zero_norm`), following a convention of similar lemmas in
 `Topology.MetricSpace.PseudoMetric` and `Topology.Algebra.Order`, the `'` version is phrased using
 \"eventually\" and the non-`'` version is phrased absolutely."]