agda-unimath
agda-unimath copied to clipboard
Complex numbers
I imagine we'd want an entire new folder for complex numbers.
This isn't near my top priorities, but it's certainly an area we can build out, and we don't need to start from real numbers at all: the Gaussian integers have plenty of material to develop. When we get to more sophisticated analysis, though, there may be some areas where it's easiest or most natural to approach problems from a complex perspective.
It would help, of course, if I noticed what is already there.
Calling this done, we can have other issues for more specific operations on the complex numbers.