Holomorphic quotient on the slit domain
ProvedWeightedRootIntegralIdentity.slitQuotientHolomorphicitycomplex-analysisholomorphicitykeyhole-contour
If the branch numerator is differentiable on a domain avoiding zero, then dividing by z preserves differentiability there.
Formal statement
import Mathlib
theorem WeightedRootIntegralIdentity.slitQuotientHolomorphicity
(G : ℂ → ℂ) (D : Set ℂ)
(hG : DifferentiableOn ℂ G D)
(hzero : ∀ z ∈ D, z ≠ 0) :
DifferentiableOn ℂ (fun z => G z / z) D := by sorry