Ordered field

An ordered field is a field \( F \) equipped with a total order \( \leq \) that is compatible with the field operations. This means that the order satisfies the following properties: 1. **Totality**: For any two elements \( a, b \in F \), one of the following holds: \( a \leq b \) or \( b \leq a \).