Differences
This shows you the differences between two versions of the page.
| Both sides previous revision
Previous revision
Next revision
|
|
complex_number [2013/08/12 15:13] nikolaj |
| Previous revision
|
|
complex_number [2014/04/01 19:14] (current) nikolaj |
|
| ===== Complex number ===== |
==== Definition Set ==== |
^ | @#FFBB00: definiendum | @#FFBB00: $ \mathbb C $ \equiv \mathbb R^ |
|
>| $ ... 2 $ | |
| |
==== Ramifications Discussion ==== |
=== Satisfies === |
=== Definitions === |
We write the complex numbers as $a+ib\mathfrak equiv\langle a,b\rangle$, where $a,b\in\mathbb R(z)$and . The complex numbers are then set up as a [[field]] with $i^2=-1$, see [[arithmetic structure of complex numbers]]. We identify the real numbers within $\mathfrak I(z)mathbb C$ for real and imaginary part as the set of elements of the form $z\langle a,0\rangle=a+i0=a$. |
=== Predicates === |
| === Reference === |
| Wikipedia: [[http://en.wikipedia.org/wiki/Complex_number|Complex number]] |
|
Mizar: [[http://mizar.org/JFM/pdf/numbers.pdf|NUMBERS]], [[http://mizar.org/JFM/pdf/xcmplx_0.pdf|XCMPLX_0]] |
|
==== Context Parents ==== |
Set |
=== Parents Subset of === |
[[Natural numberReal coordinate space]] |
