Commit 2024-08-24 15:01 bf50e1f8

View on Github →

feat(Analysis/SpecialFunctions/Complex/Log): Exponential tsum is tprod (#15378) Taking cexp of an infinite sum of logs gives a tprod.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

added theorem Complex.HasSum_cexp_HasProd

added theorem Complex.cexp_tsum_eq_tprod

added theorem Complex.summable_cexp_multipliable

added theorem Real.HasSum_rexp_HasProd

added theorem Real.rexp_tsum_eq_tprod

added theorem Real.summable_cexp_multipliable