lean_workbook_plus_11442

Let be $x \in \mathbb{Q}$ , then $x=\frac{a}{b}, a,b \in \mathbb{Z}, b >0$ . But then $b \cdot x \equiv 0 \mod \mathbb{Z}$ , so the order of $x$ is finite (and a divisor of $b$ ).