Commit 2023-12-23 06:38 a7fbc9ec

feat(Analysis/SpecialFunctions/Complex/Arg): add definition for slit plane and API, and use it (#9116) In preparation of future PRs dealing with estimates of the complex logarithm and its Taylor series, this introduces Complex.slitPlane for the set of complex numbers not on the closed negative real axis (in Analysis.SpecialFunctions.Complex.Arg), adds a bunch of API lemmas, and replaces hypotheses of the form 0 < x.re ∨ x.im ≠ 0 by x ∈ slitPlane in several other files. (We do not introduce a new file for that to avoid circular imports with Analysis.SpecialFunctions.Complex.Arg.)