Real closure

Summary

A real closure of an ordered field is a real closed algebraic extension whose order extends the given one. A real closed field is a formally real field with no proper formally real algebraic extension, such as $\R$. Every ordered field has a real closure, and it is unique up to a unique isomorphism over the field. It plays for ordered fields the role that the algebraic closure plays for fields.