In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm of an element is its distance from the zero element, see nmval: ). By this definition, the norm function is actually a norm (satisfying the properties of being a function into the reals, subadditivity/triangle inequality , absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g. Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all s in ZZ, whereas other authors (e.g. N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e. n(-x) = n(x). The definition df-ngp of a group norm follows the second aproach, see nminv.] and positive definiteness/point-separating ( n(x) = 0 <-> x = 0 ) if the structure is a metric space with a right-translation-invariant metric (see nmf, nmtri, nmvs and nmeq0). An alternate definition of a normed group (i.e. a group equipped with a norm) without using the properties of a metric space is given by theorem tngngp3. For a structure being a group, the (arbitrary) distance function can be restricted to the elements of the group without affecting the norm, see nmfval2.

Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is achieved by defining a distance function based on the norm (the distance between two elements is the norm of their difference, see ngpds: ). The operation does exactly this, i.e. it adds a distance function (and a topology) to a structure (which should be at least a group) corresponding to a given norm in the just shown way: , see also tngds. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2) resp. if the norm is in fact a norm (see tngngpd). If the norm is derived from a given metric, as done with df-nm, the induced metric is the original metric restricted to the base set: , see nrmtngdist, and the norm remains the same: , see nrmtngnrm.

- cnm
- cngp
- ctng
- cnrg
- cnlm
- cnvc
- df-nm
- df-ngp
- df-tng
- df-nrg
- df-nlm
- df-nvc
- nmfval
- nmval
- nmfval2
- nmval2
- nmf2
- nmpropd
- nmpropd2
- isngp
- isngp2
- isngp3
- ngpgrp
- ngpms
- ngpxms
- ngptps
- ngpmet
- ngpds
- ngpdsr
- ngpds2
- ngpds2r
- ngpds3
- ngpds3r
- ngprcan
- ngplcan
- isngp4
- ngpinvds
- ngpsubcan
- nmf
- nmcl
- nmge0
- nmeq0
- nmne0
- nmrpcl
- nminv
- nmmtri
- nmsub
- nmrtri
- nm2dif
- nmtri
- nmtri2
- ngpi
- nm0
- nmgt0
- sgrim
- sgrimval
- subgnm
- subgnm2
- subgngp
- ngptgp
- ngppropd
- reldmtng
- tngval
- tnglem
- tngbas
- tngplusg
- tng0
- tngmulr
- tngsca
- tngvsca
- tngip
- tngds
- tngtset
- tngtopn
- tngnm
- tngngp2
- tngngpd
- tngngp
- tnggrpr
- tngngp3
- nrmtngdist
- nrmtngnrm
- tngngpim
- isnrg
- nrgabv
- nrgngp
- nrgring
- nmmul
- nrgdsdi
- nrgdsdir
- nm1
- unitnmn0
- nminvr
- nmdvr
- nrgdomn
- nrgtgp
- subrgnrg
- tngnrg
- isnlm
- nmvs
- nlmngp
- nlmlmod
- nlmnrg
- nlmngp2
- nlmdsdi
- nlmdsdir
- nlmmul0or
- sranlm
- nlmvscnlem2
- nlmvscnlem1
- nlmvscn
- rlmnlm
- rlmnm
- nrgtrg
- nrginvrcnlem
- nrginvrcn
- nrgtdrg
- nlmtlm
- isnvc
- nvcnlm
- nvclvec
- nvclmod
- isnvc2
- nvctvc
- lssnlm
- lssnvc
- rlmnvc
- ngpocelbl