Real closed field
= Real closed field
{wiki}
A real closed field is a <formally real field> with no proper formally real algebraic extension. Equivalently every positive element in its unique compatible order is a square and every odd-degree polynomial has a root. Its positive cone is definable in the field language as the nonzero squares. The <Theory of real closed fields> is model-complete.