Complex.canonicalProduct_apply_eq_zero

@[simp]theorem canonicalProduct_apply_eq_zero {m : ℕ} {a : ℕ → ℂ}    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (m + 1))) (h_nonzero : ∀ n, a n ≠ 0) (n : ℕ) :    canonicalProduct m a (a n) = 0 := by  let f : ℕ → ℂ := fun k ↦ weierstrassFactor m (a n / a k)  have hmult : Multipliable f :=    (multipliableLocallyUniformlyOn_canonicalProduct h_sum h_nonzero).multipliable (by simp)  have htend :      Tendsto (fun N : ℕ ↦ ∏ k ∈ Finset.range N, f k) Filter.atTop        (𝓝 (canonicalProduct m a (a n))) := by    simpa [f, canonicalProduct] using hmult.hasProd.tendsto_prod_nat  have hzero :      (fun N : ℕ ↦ ∏ k ∈ Finset.range N, f k) =ᶠ[Filter.atTop] fun _ ↦ (0 : ℂ) := by    refine Filter.eventually_atTop.2 ⟨n + 1, fun N hN ↦ ?_⟩    have hnN : n ∈ Finset.range N := Finset.mem_range.mpr <| lt_of_lt_of_le (Nat.lt_succ_self n) hN    apply Finset.prod_eq_zero hnN    simp [f, h_nonzero n, weierstrassFactor_at_one]  exact tendsto_nhds_unique_of_eventuallyEq htend tendsto_const_nhds hzero