ABSTRACT
Nonzero integers may be canceled from equations, and nonzero real numbers have multiplicative inverses. The special properties are formalized in the concepts of “integral domain” and “field.” Integral domains are then characterized among all commutative, unital, and nontrivial rings by the absence of zero divisors. A finite integral domain is a field. Field structures on a set are very useful in a wide variety of contexts. The chapter discusses one typical application, to the specification of functions. The use of matrices in the construction of the field of fractions helps to minimize the number of formal verifications required, leaving only the proof of transitivity of the equivalence relation R, and confirmation of the distributive law.
