Update docstring of squeeze_one_norm' (#8667)

`squeeze_one_norm'` and `squeeze_zero_norm'` had the same docstring. The docstring of `squeeze_zero_norm'` was strictly speaking incorrect (writing `1` instead of `0`).

The docstring of `squeeze_one_norm'` was correct but perhaps this change makes it easier for people to notice the difference and what `E` is.

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."]