Table of Contents - 10.2.2. Group multiple operation
The "group multiple" operation (if the group is multiplicative, also called
"group power" or "group exponentiation" operation), can be defined for
arbitrary magmas, if the multiplier/exponent is a nonnegative integer. See
also the definition in [Lang] p. 6, where an element (of a monoid) to
the power of a nonnegative integer is defined and denoted by .
Definition df-mulg, however, defines the group multiple for arbitrary
(i.e. also negative) integers. This is meaningful for groups only, and
requires Definition df-minusg of the inverse operation .