The Order of an Element of a Group

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(G,\cdot)$ be a group, let $e$ be its identity element, unique by Uniqueness of the Identity Element and of Inverses in a Group (i), let $h^{n}$, for $h\in G$ and $n\in\mathbb{Z}$, be the integer power, and let $g\in G$.

(i) Order of an element. $g$ has finite order if $g^{n}=e$ for some $n\in\mathbb{N}$, and then the order of $g$ is the least such $n$ (it exists and is unique by Arithmetic and Order of the Natural Numbers (xv) and Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iii)),

$$\operatorname{ord}(g)=\min\{n\in\mathbb{N}:g^{n}=e\}.$$

Otherwise $g$ has infinite order.