Ordered field (source code)

= Ordered field
{wiki=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 \\).