<abstract xmlns="http://www.w3.org/1999/xhtml"><p>The use of registrations is useful in shortening Mizar proofs [1], [2], both in terms of formalization time and article space. The proposed system of classes for complex numbers aims to facilitate proofs involving basic arithmetical operations and order checking. It seems likely that the use of self-explanatory adjectives could also improve legibility of these proofs, which would be an important achievement [3]. Additionally, some potentially useful definitions, following those defined for real numbers, are introduced.</p></abstract>

The use of registrations is useful in shortening Mizar proofs [1], [2], both in terms of formalization time and article space. The proposed system of classes for complex numbers aims to facilitate proofs involving basic arithmetical operations and order checking. It seems likely that the use of self-explanatory adjectives could also improve legibility of these proofs, which would be an important achievement [3]. Additionally, some potentially useful definitions, following those defined for real numbers, are introduced.

Multiplication-Related Classes of Complex Numbers

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Multiplication-Related Classes of Complex Numbers"}

The use of registrations is useful in shortening Mizar proofs [1], [2], both in terms of formalization time and article space. The proposed system of classes...

Multiplication-Related Classes of Complex Numbers

Data publikacji: 09 sty 2021

Zakres stron: 197 - 210

Przyjęty: 31 maj 2020

DOI: https://doi.org/10.2478/forma-2020-0017

Słowa kluczowe
complex numbers, multiplication, order

© 2020 Rafał Ziobro, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Multiplication-Related Classes of Complex Numbers

Data publikacji: 09 sty 2021

Zakres stron: 197 - 210

Przyjęty: 31 maj 2020

DOI: https://doi.org/10.2478/forma-2020-0017

Słowa kluczowecomplex numbers, multiplication, order

© 2020 Rafał Ziobro, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Słowa kluczowe
complex numbers, multiplication, order