Hallo,
I stumbled across this just now and thought about it for a bit. I don't
know much about category theory, but I would say the intuitive “reason”
why complex numbers can be represented this way is the following:
1. ℂ is a field extension of ℝ with degree 2 (since it is constructed
from the
* Theorems about complex numbers are now stated only using Re and Im, the
Complex
constructor is not used anymore. It is possible to use primcorec to defined
the
behaviour of a complex-valued function.
Removed theorems about the Complex constructor from the simpset, they are
available
On Wed, 7 May 2014, Johannes Hölzl wrote:
* Theorems about complex numbers are now stated only using Re and Im, the
Complex
constructor is not used anymore. It is possible to use primcorec to defined the
behaviour of a complex-valued function.
This is also a surprising application of
