Heyting field

A Local ring $𝑅$ is a Heyting division ring iff its canonical apartness relation is tight, #m/def/ring/cons or equivalently we have

𝑥 i s n o t i n v e r t i b l e \to 𝑥 \equiv 0

#state/tidy | #lang/en | #SemBr