Remark K694
on D2134: Algebraic complex number

Worded definition of an algebraic complex number

A complex number is an algebraic complex number if and only if it is a root of a nonzero polynomial of rational coefficients.