English
From a GroupNormClass on a group α, one constructs a NormedGroup structure on α; the norm is given by the associated toNorm construction, agreeing with f on α.
Русский
Из класса GroupNormClass на группе α строится структура NormedGroup на α; норма совпадает с нормой, заданной конструктором toNorm.
LaTeX
$$$\exists s \in \text{NormedGroup}(\alpha) \text{ with } \|x\|_{s} = f(x) \ orall x \in \alpha$$$
Lean4
/-- Constructs a `NormedGroup` structure from a `GroupNormClass` on a `Group`. -/
-- See note [reducible non-instances]
@[to_additive /-- Constructs a `NormedAddGroup` structure from an `AddGroupNormClass` on an
`AddGroup`. -/
]
abbrev toNormedGroup [Group α] [GroupNormClass F α ℝ] (f : F) : NormedGroup α
where
__ := GroupSeminormClass.toSeminormedGroup f
eq_of_dist_eq_zero h := div_eq_one.mp (eq_one_of_map_eq_zero f h)
