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
