The Field of Quotients Over an Integral Domain

Christoph Schwarzweller

University of T\"ubingen

Summary.

We introduce the field of quotients over an integral domain following the well-known construction using pairs over integral domains. In addition we define ring homomorphisms and prove some basic facts about fields of quotients including their universal property.

MML Identifier: QUOFIELD

Contents (PDF format)

1. Preliminaries
2. Defining the Operations
3. Defining the Field of Quotients
4. Defining Ring Homomorphisms
5. Some Further Properties

Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[5] Jaroslaw Gryko. On the monoid of endomorphisms of universal algebra and many sorted algebra. Journal of Formalized Mathematics, 7, 1995.

[6] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.

[7] Michal Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Journal of Formalized Mathematics, 2, 1990.

[8] Michal Muzalewski. Categories of groups. Journal of Formalized Mathematics, 3, 1991.

[9] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.

[10] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[12] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[13] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

[14] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[15] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.