[isabelle-dev] Reorganising Analysis

[Lawrence Paulson]

There is plenty of material about winding numbers in Cauchy_Integral_Theorem. The theory Winding_Numbers contains more advanced and obscure results, some of which are direct consequences of the Jordan curve theorem, which is why they depend on so much other material.

Larry

> On 4 Nov 2019, at 12:48, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> Absolutely. The Residue theorem is the bare minimum of what I would expect to be included in a development of complex analysis, and that requires winding numbers.
> 
> I don't really have an idea of what material you really need for winding numbers. I recall that Wenda had some problems with them (about what happens when there's a pole on the path) – perhaps it would make sense to give that theory an overhaul altogether? Perhaps he can chime in on this; he probably knows much more about this than I do.
>