Reqmnts, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Field Properties of Complex Numbers --- Requirements

**by****Library Committee**- Received May 29, 2003
- MML identifier: ARITHM

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, ARYTM_1, RELAT_1, ARYTM_3, ORDINAL1, ORDINAL2, COMPLEX1, OPPCAT_1, XCMPLX_0; notation SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, ARYTM_0, XCMPLX_0; constructors ARYTM_0, ARYTM_1, XCMPLX_0, FUNCT_4, ARYTM_3, XBOOLE_0; clusters ARYTM_2, NUMBERS, XCMPLX_0, ARYTM_3, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE; begin :: This file contains statements which are obvious for Mizar checker if :: "requirements ARITHM" is included in the environment description :: of an article. "requirements NUMERALS" is also required. :: They are published for testing purposes only. :: Users should use appropriate requirements instead of referencing :: to these theorems. :: Some of these items need also other requirements for proper work. reserve x for complex number; theorem :: ARITHM:1 x + 0 = x; theorem :: ARITHM:2 x * 0 = 0; theorem :: ARITHM:3 1 * x = x; theorem :: ARITHM:4 x - 0 = x; theorem :: ARITHM:5 0 / x = 0; theorem :: ARITHM:6 x / 1 = x;

Back to top