The complex numbers are defined (axiomatically) in this way so that we can conveniently use the numeric constants 0, 1, 2 etc. The alternative -- using pairs of reals to represent the real and imaginary components -- would lead to the somewhat unappealing formulation of Euler's result as "exp((0,1)(pi,0)) = (-1,0)". As a matter of taste, this formalization allows the somewhat more elegant formulation: "exp(ipi) = -1".
| Theorem | Location | PVS Name | Contributors |
|---|
- David Lester, Manchester University, UK
- Anthony Narkawicz, NASA, USA
- César Muñoz, NASA, USA
- Sam Owre, SRI, USA
- Mariano Moscato, NIA & NASA, USA
- César Muñoz, NASA, USA
