ArcTan(2) a rational multiple of $\pi$? Consider a $2 \times 1$ rectangle split by a diagonal.  Then the two angles
at a corner are ArcTan(2) and ArcTan(1/2), which are about $63.4^\circ$ and $26.6^\circ$.
Of course the sum of these angles is $90^\circ = \pi/2$.
I would like to know if these angles are rational multiples of $\pi$.
It doesn't appear that they are, e.g., $(\tan^{-1} 2 )/\pi$ is computed as

0.35241638234956672582459892377525947404886547611308210540007768713728\
  85232139736632682857010522101960

to 100 decimal places by Mathematica.  But is there a theorem that could be applied here to
prove that these angles are irrational multiples of $\pi$?  Thanks for ideas and/or pointers!
(This question arose thinking about Dehn invariants.)

Lemma: If $x$ is a rational multiple of $\pi$ then $2 \cos(x)$ is an algebraic integer.
Proof
$$\cos(n+1)x+ \cos(n-1)x= 2\cos(nx)\cos(x) \,.$$
Thus
$$2\cos(n+1)x+ 2\cos(n-1)x= 2\cos(nx)2\cos(x) \,.$$
It follows from here that $2 \cos(nx)= P_n (2\cos(x))$, where $P_n$ is a monic polynomial of degree $n$ with integer coefficients.
Actually $P_{n+1}=XP_n-P_{n-1}$ with $P_1(x)=X$ and $P_0(x)=1$.
Then, if $x$ is a rational multiple of $\pi$ we have $nx =2k \pi$ for some $n$ and thus, $P_n(2 \cos(x))=1$.

Now, coming back to the problem. If $\tan(x)=2$ then $\cos(x) =\frac{1}{\sqrt{5}}$. Suppose now by contradiction that $x$ is a rational multiple of $\pi$. Then  $2\cos(x) =\frac{2}{\sqrt{5}}$ is an algebraic integer, and so is its square $\frac{4}{5}$. But this number is algebraic integer and rational, thus integer, contradiction....
P.S. If $\tan(x)$ is rational, and $x$ is a rational multiple of $\pi$, it follows exactly the same way that $\cos^2(x)$ is rational, thus $4 \cos^2(x)$ is  algebraic integer and rational. This shows that $2 \cos(x) \in \{ 0, \pm 1, \pm 2 \}$.....
