Description: Define a normed group, which is a group with a
right-translation-invariant metric. This is not a standard notion, but
is helpful as the most general context in which a metric-like norm makes
sense. (Contributed by Mario Carneiro, 2-Oct-2015)