Units of the fifth cyclotomic field are real up to roots of unity (source code)

= Units of the fifth cyclotomic field are real up to roots of unity

Let $L=\mathbb Q(\zeta_5)$ and let complex conjugation be denoted by a bar. For $u\in\mathcal O_L^\times$, every conjugate of $u/\bar u$ has modulus one, so the <kernel of the logarithmic unit embedding> shows that $u/\bar u$ is a root of unity. Reduction modulo $1-\zeta_5$ gives $u/\bar u\equiv1$, so this root belongs to $\mu_5$. Squaring permutes $\mu_5$, hence multiplication by a suitable root of unity makes $u$ real. The real unit belongs to $\mathbb Q(\sqrt5)$ and the <units of the quadratic field Q square root of five> finish the calculation.