Nonzero residues modulo a prime have multiplicative inverses

If $p$ is prime and $a\ne0$ in $\mathbb Z/p\mathbb Z$, then $aa^{-1}=1$.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_18068 (Apache-2.0).