`BookProof.ChapterCoherentOccupation.hasSum_mul_expSeries` (lam : ℝ) : HasSum (fun n : ℕ => (n : ℝ) * (lam ^ n / (n ! : ℝ))) (lam * Real.exp lam)

Initializing...

`BookProof.ChapterCoherentOccupation.hasSum_mul_expSeries` (lam : ℝ) : HasSum (fun n : ℕ => (n : ℝ) * (lam ^ n / (n ! : ℝ))) (lam * Real.exp lam) · Prove2Me