<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

Online veröffentlicht: 09. Jan. 2021

Seitenbereich: 197 - 210

Akzeptiert: 31. Mai 2020

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

Schlüsselwörter
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

Online veröffentlicht: 09. Jan. 2021

Seitenbereich: 197 - 210

Akzeptiert: 31. Mai 2020

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

Schlüsselwörtercomplex numbers, multiplication, order

© 2020 Rafał Ziobro, published by Sciendo

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

Schlüsselwörter
complex numbers, multiplication, order