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
