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 <[email protected]> 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. > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
