Formally real fields
AbstractWe 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 . In the second part of the article we define absolute values and the square root function .
|Journal series||Formalized Mathematics, ISSN 1426-2630, e-ISSN 1898-9934, (B 12 pkt)|
|Publication size in sheets||0.5|
|Keywords in English||formally real fields, ordered fields, abstract value, square root|
|License||Journal (articles only); published final; ; with publication|
|Score|| = 12.0, ArticleFromJournal|
= 12.0, ArticleFromJournal
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.