Lean now has complex numbers!
Now all we need is sine and cosine and we might be able to prove de Moivre’s theorem!
The reason I’m interested in this is that I thought that it would be interesting project to write up the proofs of all the results I stated as numbered theorems or lemmas in my M1F course. My M1F (introduction to proof) course has been one of my guides for what to work on in Lean. Of all the theorems I proved in M1F, de Moivre’s theorem (Theorem 3.2 of the course) is, I think, the only one which will need some work before it’s possible to verify it, the work in this case being a rigorous definition of the exponential function and its basic properties. I must confess that of all the other results, the hardest of them looks to me like the fundamental theorem of arithmetic — but Chris Hughes already did it! (and a whole bunch of the lemmas we needed along the way).
I feel like, other than the definitions of sine and cosine and exponential, and their basic properties, all of the M1F theorems should now be easily provable in Lean.
Xena 