<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On 4 Nov 2019, at 12:48, Manuel Eberl <<a href="mailto:eberlm@in.tum.de" class="">eberlm@in.tum.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: large; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">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?</span></div></blockquote></div><br class=""><div class="">Our definition of winding numbers is fine to me, as it follows classic analytical textbook definition which usually does not allow the target point on the path. Unless we want to further generalise the definition in a topological or algebraic direction (which does not seem too necessary at the moment), this point-on-the-path issue is probably what we have to live with. </div><div class=""><br class=""></div><div class="">My two cents about our winding numbers is the organisation: winding numbers are (kind of secretly) defined in <span class=""><a href="http://cauchy_integral_theorem.th" class="">Cauchy_Integral_Theorem.th</a>y</span><span class=""> rather than in </span><a class="list" href="https://isabelle.in.tum.de/repos/isabelle/file/c85efa2be619/src/HOL/Analysis/Winding_Numbers.thy" style="color: rgb(0, 0, 0); text-decoration: none; font-family: sans-serif;">Winding_Numbers.thy</a>, which only contains advanced facts related to winding numbers. Maybe it is worth having two theories about winding numbers — a basic one for the integral theorem and an advanced one that is on the top of Jordan_Curve & Riemann_Mapping.</div><div class=""><br class=""></div><div class="">Wenda</div></body></html>