---
tag: 778KFSM09P
kind: concept
name: Real closure
msc: [12J15, "12D15"]
sources:
  - url: https://en.wikipedia.org/wiki/Real_closed_field
---

## Summary

A real closure of an [[ordered field|0P3VCBDEE2]] is a real closed algebraic extension whose order extends the given one.
A real closed field is a [[formally real field|X32TSWJSYT]] 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|0X6AB5P3G1]] plays for fields.

## Explanations

### L1 human

The real numbers have the property that every positive number has a square root and every odd-degree polynomial has a root.
The real closure of an ordered field adds exactly what is needed to get these properties, and nothing more.
The real closure of $\Q$ is the field of real algebraic numbers, such as $\sqrt 2$ and the real cube root of $5$, but not $\pi$.