I'm trying to close some outstanding gaps in my understanding of a technique for proving an angle is irrational. While the rest of the details of the proof aren't important for my question, the short version of the proof is that if $\theta$ is a rational angle then $2 \cos(\theta)$ is an algebraic integer.
My gap in understanding has to do with proving something is an algebraic integer. Suppose $2 \cos(\theta) = \sqrt{2} - (1/2)$. If I start out with $x = \sqrt{2} - (1/2)$ and manipulate it to eliminate the $\sqrt{2}$, I wind up with $4x^2 +4x - 7 = 0$. This also happens to be the same polynomial that Wolfram Alpha tells me is the minimal polynomial for $\sqrt{2} - (1/2)$.
Now I look at $4x^2 +4x - 7$ and see the leading $4$ and conclude that it isn't monic so $\sqrt{2} - (1/2)$ isn't an algebraic integer.
But when I check Wikipedia and many other sources I see the definition of the minimal polynomial is:
The minimal polynomial of $\alpha$ is the monic polynomial of least degree among all polynomials in $F[x]$ having $\alpha$ as a root
This seems to imply that for any value $\alpha$ you can find a monic polynomial.
My hunch is that the difference has to do with allowing coefficients to be in the rationals $\mathbb{Q}$ instead of the integers $\mathbb{Z}$ but I'm not certain.
What's going on here? Why do I (and Wolfram Alpha) not get a monic minimum polynomial and why does the minimum polynomial definition seem to suggest I should. Is the difference really just polynomials with coefficients in $\mathbb{Q}$ versus $\mathbb{Z}$ or is there something more subtle going on here?
Finally, is the argument I outlined above sufficient to prove that $2 \cos(\theta) = \sqrt{2} - (1/2)$ implies $\theta$ isn't a rational angle?
Basically, the minimal polynomial for $\alpha$ over $\Bbb Q$ is the polynomial $f(x)$ having rational coefficients and smallest degree such that $f(\alpha)=0$.
Problem is, this does not give a unique polynomial: if $f$ satisfies these requirements then so does any (non-zero) constant times $f$. So, if we want to get a single definite minimal polynomial, we have to standardise it somehow. There are two common ways of doing this.
Which do you use? Really doesn't matter. It should not be hard to convince yourself that the two methods are equivalent. Sometimes people use the terminology that the first gives the "minimal polynomial of $\alpha$ over $\Bbb Q$" and the second gives the "minimal polynomial of $\alpha$ over $\Bbb Z$".
It appears that Wikipedia is using the former definition and Wolfram Alpha is using the latter.