Theorem Real.rexp_tsum_eq_tprod

Modification history

2024-08-24 15:01

Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

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

Added Real.rexp_tsum_eq_tprod View on Github →