<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

Publicado en línea: 09 ene 2021

Páginas: 197 - 210

Aceptado: 31 may 2020

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

Palabras clave
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

Publicado en línea: 09 ene 2021

Páginas: 197 - 210

Aceptado: 31 may 2020

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

Palabras clavecomplex numbers, multiplication, order

© 2020 Rafał Ziobro, published by Sciendo

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

Palabras clave
complex numbers, multiplication, order