English
From a GroupSeminormClass on a commutative group α, one obtains a SeminormedCommGroup structure on α, whose underlying seminormed group is induced by the given f and whose multiplication is commutative.
Русский
Из класса GroupSeminormClass на коммутативной группе α получают структуру SeminormedCommGroup на α, основанную на заданном f и с коммутативной операцией умножения.
LaTeX
$$$\exists \mathcal{S} \in \text{SeminormedCommGroup}(\alpha) \ \text{such that } (\|x\|)_{\mathcal{S}} = f(x) \text{ for all } x\in\alpha$$$
Lean4
/-- Constructs a `SeminormedCommGroup` structure from a `GroupSeminormClass` on a `CommGroup`. -/
-- See note [reducible non-instances]
@[to_additive /-- Constructs a `SeminormedAddCommGroup` structure from an `AddGroupSeminormClass`
on an `AddCommGroup`. -/
]
abbrev toSeminormedCommGroup [CommGroup α] [GroupSeminormClass F α ℝ] (f : F) : SeminormedCommGroup α
where
__ := GroupSeminormClass.toSeminormedGroup f
__ : CommGroup α := inferInstance
