Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Tytuł: Rings of Fractions and Localization
Autorzy: Watase, Yasushige
Słowa kluczowe: rings of fractions
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
DOI: 10.2478/forma-2020-0006
ISSN: 1426-2630
e-ISSN: 1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2020, Volume 28, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2020_28_01_0006.pdf268,19 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons