Let $\zeta_n$ be a primitive $n$th root of unity. I want to show that $F_n := \mathbb{Q}\left(\zeta_n\right)\cap\mathbb{R} = \mathbb{Q}\left(\zeta_n + \zeta_n^{-1}\right) = \mathbb{Q}\left(\cos\left(\frac{2\pi}{n}\right)\right)$ and then to calculate $\left[\mathbb{Q}\left(\zeta_n\right) : F_n\right]$ and $m_{\zeta_n}^{F_n}$.
I have solved it, but I'm not sure how to formalize it. Here is my solution:
We have $\zeta_2 = -1$, so $\mathbb{Q}\left(\zeta_2\right) = \mathbb{Q}$, and since $\cos\left(\frac{2\pi}{2}\right) = -1$, $F_2 := \mathbb{Q}$. Hence $\left[\mathbb{Q}\left(\zeta_2\right) : F_2\right] = 1$ and $m_{\zeta_2}^{F_2} = x + 1$ (I don't really know how to improve what I wrote in this case).
Now let $n > 2$. We can suppose without loss of generality that $\zeta_n = e^{\frac{2\pi i}{n}}$ (I don't know how to justify this), and then $$\zeta_n + \zeta_n^{-1} = e^{\frac{2\pi i}{n}} + e^{-\frac{2\pi i}{n}} = 2\cos\left(\frac{2\pi}{n}\right) \in \mathbb{R}$$ (is there a better way to write or to justify this equality?). Thus we have $\mathbb{Q}\left(\zeta_n + \zeta_n^{-1}\right) = \mathbb{Q}\left(\cos\left(\frac{2\pi}{n}\right)\right)$ (I would like to complete this…). Since $\zeta_n + \zeta_n^{-1} \in \mathbb{Q}\left(\zeta_n\right)\cap\mathbb{R}$, $\mathbb{Q}\left(\zeta_n + \zeta_n^{-1}\right) \subseteq \mathbb{Q}\left(\zeta_n\right)\cap\mathbb{R}$. In order to see the other inclusion, we observe that $m_{\zeta_n}^{\mathbb{Q}\left(\zeta_n + \zeta_n^{-1}\right)}(x) = x² - \left(\zeta_n + \zeta_n^{-1}\right)x + 1$ (how can I justify that this polynomial is irreducible over $\mathbb{Q}\left(\zeta_n + \zeta_n^{-1}\right)$?). So $\left[\mathbb{Q}\left(\zeta_n\right) : \mathbb{Q}\left(\zeta_n + \zeta_n^{-1}\right)\right] = 2$.
Now I want to write that the minimal polynomial is the same to $\mathbb{Q}\left(\zeta_n\right)|\mathbb{Q}\left(\zeta_n\right)\cap\mathbb{R}$ in order to finish the problem.
Would you help me completing this formalization, please? Thank you so much!
All the primitive $n$th roots of unity are conjugate, indistinguishable up to field isomorphism. It does not matter which you adjoin. In writing $K(\alpha)$, what do we really mean? In abstraction this often just means $K[x]/(m)$ where $m$ is some irreducible polynomial and $\alpha$ is understood to be a formal root of $m$. $\Bbb Q(\zeta_n)\cong\Bbb Q[x]/(\Phi_n)\cong\Bbb Q(\zeta_n')$ where $\zeta'_n$ is any other primitive $n$th root of unity. It does not matter at all if you take $\exp(2\pi i/n)$ or not (in this case you can also see the extension is normal, $\zeta_n$ is contained in and generates $\Bbb Q(\zeta'_n)$ so the two fields $\Bbb Q(\zeta'_n),\Bbb Q(\zeta_n)$ can be viewed as literally the same qua subfields of $\Bbb C$).
Since the polynomial is quadratic, that amounts to justifying that the polynomial has no roots in this field. That's equivalent to saying that $\Bbb Q(\zeta_n)$ strictly contains $\Bbb Q(\zeta_n+\zeta_n^{-1})\subseteq\Bbb Q(\zeta_n)\cap\Bbb R$. If you think about real and imaginary parts, this is "obvious" but that approach doesn't feel very general, unfortunately (edit: this can be understood to be for general reasons; $\mathrm{Gal}(\Bbb Q(\zeta_n);\Bbb Q)$ contains a complex conjugation automorphism $\sigma$ whose order is $2$; $\Bbb Q(\zeta_n)\cap\Bbb R$ is the fixed field of $\langle\sigma\rangle$ and because the group is nontrivial we know this fixed field must be a proper subfield)).
I recommend the following. $\Bbb Q(\zeta_n)\supsetneq\Bbb Q(\zeta_n)\cap\Bbb R\supseteq\Bbb Q(\zeta_n+\zeta_n^{-1})$ tells you the relevant extension degrees are $2$ and some number $1<[\Bbb Q(\zeta_n):\Bbb Q(\zeta_n)\cap\Bbb R]\le2$ so we must have equality with $2$ and $\Bbb Q(\zeta_n+\zeta_n^{-1})=\Bbb Q(\zeta_n)\cap\Bbb R$. Then it follows that the minimal polynomial you want must be the one you already wrote down.