Lean-Workbook Plus 9607: Trigonometric identity

Prove that the roots of the equation $\sin x = 0$ are $n\pi$ where $n \in \mathbb{Z}$.

Source: Lean-Workbook row lean_workbook_plus_9607 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.