---
tag: 2362AFNG8X
kind: definition
name: Formally real field
msc: ["12D15", 12J15]
defines: X32TSWJSYT
uses: [0QA8CHH8MG, 010JCV9J4E, 1ZB13N78XW, 01CJRJKDAA]
sources:
  - url: https://en.wikipedia.org/wiki/Formally_real_field
---

## Definition

Let $F$ be a [[field|0QA8CHH8MG]].
The field $F$ is *formally real* if $-1$ is not a sum of squares in $F$.
That is, there are no $n \ge 1$ and $a_1, \dots, a_n \in F$ with $a_1^2 + \cdots + a_n^2 = -1$.

## Remarks

Equivalently, for all $n \ge 1$ and $a_1, \dots, a_n \in F$, if $a_1^2 + \cdots + a_n^2 = 0$, then $a_1 = \cdots = a_n = 0$.
By the Artin–Schreier theorem on orderings, $F$ is formally real if and only if $F$ carries a structure of [[ordered field|010JCV9J4E]].
A formally real field has [[characteristic|1ZB13N78XW]] $0$, since in characteristic $p$ one has $-1 = 1^2 + \cdots + 1^2$ with $p - 1$ terms.
Example: $\Q$ is formally real, because a sum of rational squares is at least $0$ in the usual order.
Non-example: $\C$ is not formally real, because $-1 = i^2$; this is why [[$\C$ cannot be ordered|01CJRJKDAA]].