Commit 2025-07-05 10:03 de46d239

View on Github →

Add the Mittag-Leffler expansion for cotangent (#26006) This PR continues the work from #25448. Original PR: https://github.com/leanprover-community/mathlib4/pull/25448

Estimated changes

Modified Mathlib/Analysis/Complex/IntegerCompl.lean

added theorem Complex.integerComplement_pow_two_ne_pow_two

Modified Mathlib/Analysis/Complex/LocallyUniformLimit.lean

modified theorem Complex.logDeriv_tendsto

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

deleted theorem Real.multipliable_one_add_of_summable

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

added theorem HasProdLocallyUniformlyOn_euler_sin_prod

added theorem HasProdUniformlyOn_sineTerm_prod_on_compact

added theorem Summable_cotTerm

added theorem cotTerm_identity

added theorem cot_series_rep'

added theorem cot_series_rep

added theorem euler_sineTerm_tprod

added theorem logDeriv_prod_sineTerm_eq_sum_cotTerm

added theorem logDeriv_sin_div_eq_cot

added theorem logDeriv_sineTerm_eq_cotTerm

added theorem multipliableUniformlyOn_euler_sin_prod_on_compact

added theorem multipliable_sineTerm

added theorem sin_pi_z_ne_zero

added theorem sineTerm_ne_zero

added theorem tendsto_euler_sin_prod'

added theorem tendsto_logDeriv_euler_cot_sub

added theorem tendsto_logDeriv_euler_sin_div