Solution (source code)

= Solution

An element is algebraic over $F$ when some nonzero <polynomial> in $F[x]$ vanishes at it. Its <minimal polynomial> is the <monic polynomial> of least positive <degree> with this property; scaling a least-<degree> nonzero vanishing <polynomial> makes it monic.

If $m_1,m_2$ are two such <polynomials>, they have the same least <degree>. Their difference has smaller <degree> because both are monic, and it also vanishes at $a$. Minimality forces the difference to be zero. Hence \b[the monic <minimal polynomial> is unique].