normed_group.of_add_dist

Construct a normed group from a translation invariant distance

normed_group.of_add_dist'

Construct a normed group from a translation invariant distance

normed_group.core

A normed group can be built from a norm that satisfies algebraic properties. This is formalised in this structure.

rescale_to_shell

If there is a scalar c with ∥c∥>1, then any element can be moved by scalar multiplication to any shell of width ∥c∥. Also recap information on the norm of the rescaling element that shows up in applications.