- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
An algebraically closed field of nonzero characteristic has no finite-index subfields.
Let \(R\) be a real field with no nontrivial real algebraic extensions. Then \(R\) is real closed.
An algebraically closed field of characteristic 0 has an index-2 real closed subfield.
Let \(F\) be an ordered field with a real closure \(R\), and let \(K/F\) be a finite ordered extension. Then there is a unique order-preserving \(F\)-homomorphism \(K\to R\).
Let \(F\) be an ordered field with a real closure \(R\), and let \(K/F\) be a finite ordered extension. Then there is an \(F\)-homomorphism \(K\to R\).
Let \(F\) be an ordered field with real closure \(R\), and let \(K/F\) be algebraic. Then field orderings on \(K\) making \(K/F\) ordered correspond to \(F\)-homomorphisms \(K\to R\) via the order obtained by restriction from \(R\).
Let \(F\) be an ordered field, and let \(a\in F\). Then there is a unique ordering on the function field \(F(X)\) making \(F(X)/F\) ordered such that \(X{\gt}a\) but \(b{\gt}X\) for \(b{\gt}a\), and a unique one such that \(X{\lt}a\) but \(b{\lt}X\) for \(b{\lt}a\).
\(R\) has no nontrivial ordered algebraic extensions (with respect to the unique order).
An field \(F\) is real closed iff
for all nonzero \(x\) in \(F\), exactly one of \(x\) and \(-x\) is a square, and
every odd-degree polynomial over \(F\) has a root in \(F\).
An ordered field is real closed iff
every non-negative element is a square, and
every odd-degree polynomial over \(F\) has a root in \(F\).
\(R\) has a unique ordering making it an ordered field. In this ordering, the non-negative elements are exactly the squares.
The finite-index subfields of \(\bar{\mathbb {Q}}\) are isomorphic copies of \(\mathbb {Q}_{\text{alg}}=\bar{\mathbb {Q}}\cap \mathbb {R}\) indexed by \(\operatorname{Gal}(\mathbb {Q}_{\text{alg}}/\mathbb {Q}(i))\).
Let \(R\) be a field. TFAE:
\(R\) is real closed.
\(\bar{R}=R(i)\) (and \(-1\) is not a square in \(R\)).
\(R\) is real, but has no nontrivial real algebraic extensions.
Let \(R\) be an ordered field. TFAE:
\(R\) is real closed.
Polynomials over \(R\) satisfy the intermediate value property.
\(R\) is maximal with respect to ordered algebraic extensions.
Let \(F\) be an ordered field. Then the real closure of \(F\) is unique up to unique \(F\)-isomorphism.
Let \(F\) be an ordered field, and let \(f\) be a polynomial over \(F\). Then \(f\) has the same number of roots in any real closure of \(F\).