English
From a GroupNormClass on a commutative group α, one constructs a NormedCommGroup structure on α; the underlying NormedGroup part is inherited from the normed group construction.
Русский
Из GroupNormClass на коммутативной группе α строится структура NormedCommGroup на α; базовая часть NormedGroup наследуется от соответствующего построения.
LaTeX
$$$\exists s \in \text{NormedCommGroup}(\alpha) \text{ with } \|x\|_{s} = f(x) \; \forall x$$$
Lean4
/-- Constructs a `NormedCommGroup` structure from a `GroupNormClass` on a `CommGroup`. -/
-- See note [reducible non-instances]
@[to_additive /-- Constructs a `NormedAddCommGroup` structure from an `AddGroupNormClass` on an
`AddCommGroup`. -/
]
abbrev toNormedCommGroup [CommGroup α] [GroupNormClass F α ℝ] (f : F) : NormedCommGroup α
where
__ := GroupNormClass.toNormedGroup f
__ : CommGroup α := inferInstance
