The Logarithmic derivative of an infinite product

We show that if we have an infinite product of functions f that is locally uniformly convergent, then the logarithmic derivative of the product is the sum of the logarithmic derivatives of the individual functions.

theorem logDeriv_tprod_eq_tsum {ι : Type u_1} {s : Set ℂ} (hs : IsOpen s) {x : ℂ} (hx : x ∈ s) {f : ι → ℂ → ℂ} (hf : ∀ (i : ι), f i x ≠ 0) (hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s) (hm : Summable fun (i : ι) => logDeriv (f i) x) (htend : MultipliableLocallyUniformlyOn f s) (hnez : ∏' (i : ι), f i x ≠ 0) : logDeriv (fun (x : ℂ) => ∏' (i : ι), f i x) x = ∑' (i : ι), logDeriv (f i) x