Definition·D043
Powers of a group element
Repeated application of the group operation: the zeroth power is the identity, and each next power multiplies by the element once more.
Fix a group
with identity
, and let
. The powers of
are defined by
for every
. These two equations determine one and only one function
, written
.
In words
The zeroth power of any element is the identity, and each next power multiplies by g on the right one more time. These two rules pin the powers down uniquely.
Rests onA02
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
For a fixed
this is the recursion theorem with start value
and step rule
, with
the successor, the same shape that makes multiplication iterate addition; every value stays in
because
is a binary operation on
. Bundling the powers of all
at once into a single function
is a Separation step, exactly as for addition and multiplication. Because the exponents are the naturals, only nonnegative powers are available here; the inverse
comes from L28 instead, and a two-sided power law over all integer exponents would need the integers, which this library has not constructed. The powers of a single element are the raw material of its order and of the cyclic subgroup it generates.