An ordered field is a \reftext{def:field-c54-2026b}{field} $F$ together with a binary relation $\le$ on $F$ such that $\le$ is a \reftext{def:total-order-c54-2026a}{total order} on $F$, and the order is compatible with the field operations in the following sense.

1. For all $a,b,c\in F$, if $a\le b$, then $a+c\le b+c$.
2. For all $a,b\in F$, if $0\le a$ and $0\le b$, then $0\le ab$.