English
A GroupNorm E induces a NormedGroup on E by taking the same underlying structure with the norm as the group norm and the distance dist x y = ∥x y^{-1}∥.
Русский
GroupNorm E порождает NormedGroup на E, расстояние определяется как dist(x,y)=∥x y^{-1}∥ и нормa как нормa группы.
LaTeX
$$$\text{GroupNorm.toNormedGroup}$ gives a NormedGroup with dist(x,y)=‖x y^{-1}‖ and ∥x∥=dist(x,1).$$
Lean4
/-- Construct a normed group from a norm, i.e., registering the distance and the metric space
structure from the norm properties. Note that in most cases this instance creates bad definitional
equalities (e.g., it does not take into account a possibly existing `UniformSpace` instance on
`E`). -/
@[to_additive /-- Construct a normed group from a norm, i.e., registering the distance and the metric
space structure from the norm properties. Note that in most cases this instance creates bad
definitional equalities (e.g., it does not take into account a possibly existing `UniformSpace`
instance on `E`). -/
]
abbrev toNormedGroup [Group E] (f : GroupNorm E) : NormedGroup E :=
{ f.toGroupSeminorm.toSeminormedGroup with eq_of_dist_eq_zero := fun h => div_eq_one.1 <| eq_one_of_map_eq_zero f h }
-- See note [reducible non-instances]
