Heyting field

A Heyting field is one of the inequivalent ways in constructive mathematics to capture the classical notion of a field. It is essentially a field with an apartness relation. The key field axiom is that an element is invertible if and only if it is not zero. In a Heyting field, this is taken to mean that it is apart from zero. In many cases, the assumption that an element is not equal to zero is insufficient to construct the inverse; the assumption that it is apart from zero implicitly contains the necessary information.

The prototypical Heyting field is the real numbers with their natural apartness relation.