Theorem Complex.HasSum_cexp_HasProd

Modification history

2024-08-24 15:01

Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

feat(Analysis/SpecialFunctions/Complex/Log): Exponential tsum is tprod (#15378) …

Added Complex.HasSum_cexp_HasProd View on Github →