Documentation

LeanPool.LeanModularForms.Modularforms.Cotangent

Cotangent series expansion #

All of the lemmas formerly defined here — Complex.cot_eq_exp_ratio, Complex.cot_pi_eq_exp_ratio, pi_mul_cot_pi_q_exp, the sinTerm/cotTerm series, tendsto_logDeriv_euler_*, cot_series_rep/cot_series_rep', and the lemmas building up to them — have been upstreamed into Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent. This file is now a re-export so the historical import path continues to work.

The two downstream consumers in this project (Modularforms/summable_lems.lean) already import the upstream module directly and resolve cot_series_rep' and pi_mul_cot_pi_q_exp against Mathlib's versions.