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.Analysis.Normed.Order.Hom.Ultra
for further upgrades to nonarchimedean normed groups.
Constructs a SeminormedGroup
structure from a GroupSeminormClass
on a Group
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructs a SeminormedAddGroup
structure from an AddGroupSeminormClass
on an
AddGroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructs a SeminormedCommGroup
structure from a GroupSeminormClass
on a CommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructs a SeminormedAddCommGroup
structure from an AddGroupSeminormClass
on an
AddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructs a NormedGroup
structure from a GroupNormClass
on a Group
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructs a NormedAddGroup
structure from an AddGroupNormClass
on an
AddGroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructs a NormedCommGroup
structure from a GroupNormClass
on a CommGroup
.
Equations
- GroupNormClass.toNormedCommGroup f = { toNorm := NormedGroup.toNorm, toGroup := NormedGroup.toGroup, mul_comm := ⋯, toMetricSpace := NormedGroup.toMetricSpace, dist_eq := ⋯ }
Instances For
Constructs a NormedAddCommGroup
structure from an AddGroupNormClass
on an
AddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.