## Definition ## In a [[ring]] $A$, multiplication is a [[power-associative magma]], and thus $A$ has: * A binary power function ${(-)}^{(-)}: A \times \mathbb{N} \to A$ * Two families of dependent terms of identities $$a:A \vdash i(a): a^1 = a$$ $$m:\mathbb{N}, n:\mathbb{N}, a:A \vdash c(m, n, a): (a^m)^n = a^{m \cdot n}$$ stating that the power is a right multiplicative $\mathbb{N}$-[[action]]. * A family of dependent terms of identities $$a:A, m:\mathbb{N}, n:\mathbb{N} \vdash \pi(a, m, n):\mu(a^m, a^n)=a^{m+n}$$ representing the law of exponents for the multiplicative magma. ## See also ## * [[polynomial function]] * [[ring]]