I'm not an expert in complex analysis either, but do remember that it was briefly mentioned – but not proved – in my introductory lecture on Complex Analysis when I was an undergratuate.
My intuition tells me that this is a very beautiful result, but not one that you need a lot, but I could be wrong about this. I could perhaps ask around a bit. I for one am quite open to the idea of moving more material from the distribution to the AFP, especially from HOL-Analysis. Picard's theorem sounds like a reasonable candidate for that, but in general, I also have no idea where to draw the line. Cheers, Manuel On 22/02/17 17:46, Lawrence Paulson wrote: > I have just added this to the Analysis directory, making its inevitable > refactoring more necessary. > > Arguably it should be an AFP entry. Unfortunately, I’m not sufficiently > expert in complex analysis to say whether it is core material or not. It > looks like a fundamental result to me. > > We should probably resolve the question of Analysis before the next release. > How do we decide which things go into Complex_Main versus Analysis (which > could be split into basic/advanced) and the AFP? > > Larry > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
