Formally Real Fields

Christoph Schwarzweller

doi:10.1515/forma-2017-0024

.blurhash-client-img { display: none !important; }

Formally Real Fields

Formalized Mathematics

Volume 25 (2017): Issue 4 (December 2017)

By: Christoph Schwarzweller

Open Access

|Mar 2018

Abstract

We extend the algebraic theory of ordered fields [7, 6] in Mizar [1, 2, 3]: we show that every preordering can be extended into an ordering, i.e. that formally real and ordered fields coincide.We further prove some characterizations of formally real fields, in particular the one by Artin and Schreier using sums of squares [4]. In the second part of the article we define absolute values and the square root function [5].

References

[1] Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: 10.1007/978-3-319-20615-8 17.10.1007/978-3-319-20615-817
Open DOI Search in Google Scholar Back to article
[2] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. doi: 10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1
Open DOI Search in Google Scholar Back to article
[3] Adam Grabowski, Artur Korniłowicz, and Christoph Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Infor mation Systems (FedCSIS), volume 8 of Annals of Computer Science and Information Systems, pages 363-371, 2016. doi: 10.15439/2016F520.10.15439/2016F520
Search in Google Scholar Back to article
[4] Nathan Jacobson. Lecture Notes in Abstract Algebra, III. Theory of Fields and Galois Theory. Springer-Verlag, 1964.
Search in Google Scholar Back to article
[5] Manfred Knebusch and Claus Scheiderer. Einf¨uhrung in die reelle Algebra. Vieweg-Verlag, 1989.10.1007/978-3-322-85033-1
Search in Google Scholar Back to article
[6] Alexander Prestel. Lectures on Formally Real Fields. Springer-Verlag, 1984.10.1007/BFb0101548
Search in Google Scholar Back to article
[7] Knut Radbruch. Geordnete K¨orper. Lecture Notes, University of Kaiserslautern, Germany, 1991.
Search in Google Scholar Back to article
[8] Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559-564, 2001.
Search in Google Scholar Back to article
[9] Christoph Schwarzweller. Ordered rings and fields. Formalized Mathematics, 25(1):63-72, 2017. doi: 10.1515/forma-2017-0006.10.1515/forma-2017-0006
Open DOI Search in Google Scholar Back to article
[10] Christoph Schwarzweller. On roots of polynomials and algebraically closed fields. Formalized Mathematics, 25(3):185-195, 2017. doi: 10.1515/forma-2017-0018.10.1515/forma-2017-0018
Search in Google Scholar Back to article
[11] Christoph Schwarzweller and Artur Korniłowicz. Characteristic of rings. Prime fields. Formalized Mathematics, 23(4):333-349, 2015. doi: 10.1515/forma-2015-0027.10.1515/forma-2015-0027
Open DOI Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.1515/forma-2017-0024 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 249 - 259

Submitted on: Nov 29, 2017

Published on: Mar 28, 2018

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

Related subjects:

Computer sciences, other

© 2018 Christoph Schwarzweller, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.

Volume 25 (2017): Issue 4 (December 2017)