<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

Published Online: Jan 09, 2021

Page range: 197 - 210

Accepted: May 31, 2020

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

Keywords
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

Published Online: Jan 09, 2021

Page range: 197 - 210

Accepted: May 31, 2020

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

Keywordscomplex numbers, multiplication, order

© 2020 Rafał Ziobro, published by Sciendo

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

Keywords
complex numbers, multiplication, order