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
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.