Constructing (semi)normed groups from (semi)normed homs #
This file defines constructions that upgrade (Comm)Group
to (Semi)Normed(Comm)Group
using a Group(Semi)normClass
when the codomain is the reals.
See Mathlib.Algebra.Order.Hom.Ultra
for further upgrades to nonarchimedean normed groups.
Constructs a SeminormedAddGroup
structure from an AddGroupSeminormClass
on an
AddGroup
.
Instances For
Constructs a SeminormedGroup
structure from a GroupSeminormClass
on a Group
.
Equations
Instances For
Constructs a SeminormedAddCommGroup
structure from an AddGroupSeminormClass
on an
AddCommGroup
.
Instances For
Constructs a SeminormedCommGroup
structure from a GroupSeminormClass
on a CommGroup
.
Instances For
Constructs a NormedAddGroup
structure from an AddGroupNormClass
on an
AddGroup
.
Equations
Instances For
Constructs a NormedGroup
structure from a GroupNormClass
on a Group
.
Equations
Instances For
Constructs a NormedAddCommGroup
structure from an AddGroupNormClass
on an
AddCommGroup
.
Equations
Instances For
Constructs a NormedCommGroup
structure from a GroupNormClass
on a CommGroup
.