Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/9224
Tytuł: | Rings of Fractions and Localization |
Autorzy: | Watase, Yasushige |
Słowa kluczowe: | rings of fractions localization total-quotient ring quotient field |
Data wydania: | 2020 |
Data dodania: | 10-cze-2020 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 28, Issue 1, Pages 79-87 |
Abstrakt: | 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. |
Afiliacja: | Suginami-ku Matsunoki, 3-21-6 Tokyo, Japan |
URI: | http://hdl.handle.net/11320/9224 |
DOI: | 10.2478/forma-2020-0006 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | http://creativecommons.org/licenses/by-sa/3.0/pl/ |
Występuje w kolekcji(ach): | Formalized Mathematics, 2020, Volume 28, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2020_28_01_0006.pdf | 268,19 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL