Rings of Fractions and Localization

Summary This article formalized rings of fractions in the Mizar system [3], [4]. A construction of the ring of fractions from an integral domain, namely a quotient field was formalized in [7]. This article generalizes a construction of fractions to a ring which is commutative and has zero divisor by means of a multiplicatively closed set, say S , by known manner. Constructed ring of fraction is denoted by S ~ R instead of S − 1 R appeared in [1], [6]. As an important example we formalize a ring of fractions by a particular multiplicatively closed set, namely R \ p, where p is a prime ideal of R . The resulted local ring is denoted by R p . In our Mizar article it is coded by R ~ p as a synonym. This article contains also the formal proof of a universal property of a ring of fractions, the total-quotient ring, a proof of the equivalence between the total-quotient ring and the quotient field of an integral domain.