This file provides the action of a unit on a type
has_scalar (units M) α, in the presence of
has_scalar M α, with the obvious definition stated in
units.smul_def. This definition preserves
distrib_mul_action structures too.
mul_action G M for some group
G satisfying some additional properties admits a
mul_action G (units M) structure, again with the obvious definition stated in
These instances use a primed name.