Complex.canonicalProduct_ne_zero

theorem canonicalProduct_ne_zero {m : ℕ} {a : ℕ → ℂ}    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (m + 1))) (h_nonzero : ∀ n, a n ≠ 0)    {z : ℂ} (hz : z ∉ Set.range a) :    canonicalProduct m a z ≠ 0 := by  let f : ℕ → ℂ := fun n ↦ weierstrassFactor m (z / a n) - 1  have hfn : ∀ n, 1 + f n ≠ 0 := by    intro n    have hza : z ≠ a n := by      intro hza      exact hz ⟨n, hza.symm⟩    simpa [f] using (weierstrassFactor_div_ne_zero_iff (m := m) (a := a n) (z := z)      (h_nonzero n)).2 hza  have hnormsumm :      Summable (fun n : ℕ ↦ ‖weierstrassFactor m (z / a n) - 1‖) :=    summable_norm_weierstrassFactor_div_sub_one_of_summable_inv_pow      (m := m) (a := a) h_sum h_nonzero z  simpa [canonicalProduct, f] using    (tprod_one_add_ne_zero_of_summable (f := f) hfn hnormsumm)