The principal root of one has unit norm

For every natural $n\ne0$, the principal complex power satisfies $|1^{1/n}|=1$.

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