Axiomatic WikiWWikiDDefinitionsPowers of an integer
Definition·D119
The k-th power of an integer, defined by repeated multiplication starting from 1.
Fix
. The powers of
are defined by
for every
, with
(D057),
the successor, and
integer multiplication. These two equations determine a unique function
, written
.
In words
The zeroth power of any integer is 1, and each next power multiplies by x once more.
Rests onA02
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 · A09 (computed from the citation graph, not asserted).
Remarks
For a fixed
this is the recursion theorem with start value
and step rule
, the same shape that makes D028 iterate D027 and group powers iterate the group operation. Only nonnegative exponents are available, since the exponent ranges over
. The index laws
and
hold by induction on
, exactly as for L32. This is the power in the multiplicative monoid of the ring
; for a class that is a unit modulo
it agrees with the group power in
(L79), the fact behind Euler and Fermat.