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. Manuel On 04/11/2019 13:44, Lawrence Paulson wrote: > Then the obvious stopping point is one line above: Derivative. > > The problem at the moment with basing a development around the Cauchy > integral theorem is that you might also want to include Winding_Numbers, but > that theory inherits almost the whole of Analysis: even the Jordan curve > theorem. > > Larry > >> On 4 Nov 2019, at 12:19, Manuel Eberl <[email protected]> wrote: >> >> Great work, thanks for taking care of this! >> >> Just abstractly speaking, it would seem very odd to me to have a "complex >> analysis" directory without integration. Complex integration and the Cauchy >> integral formula are such basic tools in complex analysis that not including >> them in a "complex analysis" entry would seem… unusual to me. >> >> Perhaps "complex analysis prerequisites". >>
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
