Units of a Monoid: Unique Inverses, Products, and the Group of Units

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(M,\cdot)$ be a monoid with identity $e$, with products written $uv$ as in Semigroups (i), and let units and their inverses be as in Units of a Monoid (i).

(i) Uniqueness of inverses. Every unit $u$ of $M$ has exactly one inverse, written $u^{-1}$.

(ii) The identity. $e$ is a unit, and $e^{-1}=e$.

(iii) Products of units. If $u$ and $v$ are units, then $uv$ is a unit and

$$(uv)^{-1}=v^{-1}u^{-1}.$$

(iv) Inverses of units. If $u$ is a unit, then $u^{-1}$ is a unit and $(u^{-1})^{-1}=u$.

(v) The group of units. The set $M^{\times}$ of units of $M$ (Units of a Monoid (ii)), with the restriction of $\cdot$ to $M^{\times}\times M^{\times}$, is a group with identity $e$.