Complex.Hadamard.divisor_hadamardDenom_eq

theorem divisor_hadamardDenom_eq    (m : ℕ) {f : ℂ → ℂ} (hf : Differentiable ℂ f)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    MeromorphicOn.divisor (hadamardDenom m f) (Set.univ : Set ℂ) =      MeromorphicOn.divisor f (Set.univ : Set ℂ) := by  ext z  have hden_entire : Differentiable ℂ (hadamardDenom m f) :=    differentiable_hadamardDenom (m := m) f h_sum  have hf_entire : Differentiable ℂ f := hf  have hden :      (MeromorphicOn.divisor (hadamardDenom m f) (Set.univ : Set ℂ)) z =        (analyticOrderNatAt (hadamardDenom m f) z : ℤ) := by    simpa using (divisor_univ_eq_analyticOrderNatAt_int (f := hadamardDenom m f) hden_entire z)  have hfz :      (MeromorphicOn.divisor f (Set.univ : Set ℂ)) z =        (analyticOrderNatAt f z : ℤ) := by    simpa using (divisor_univ_eq_analyticOrderNatAt_int (f := f) hf_entire z)  simp [hden, hfz, analyticOrderNatAt_hadamardDenom_eq (m := m) (hf := hf) (h_sum := h_sum) z]