Theorem: Complex.exp_tsum_primes (EulerProducts/Logarithm.lean)

State before:
f : ℕ → ℂ
hsum : Summable f
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (f p)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), f ↑p)))
Tactic:
simpa only [← exp_sum] using Tendsto.cexp <| tendsto_sum_primesBelow_tsum hsum
State after:
no goals