HasSumUniformlyOn / cotTerm scratch file #
This file was an early scratch pad where Chris Birkbeck staged a long sequence of helper
lemmas en route to results on HasSumUniformlyOn and on the cotangent product expansion.
Almost every lemma here has since been upstreamed (under the same or a slightly different
name) into Mathlib (Mathlib.Analysis.Series.LocallyUniform,
Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent,
Mathlib.Analysis.Complex.LocallyUniformLimit, etc.). The remaining purely-local helpers
were not imported by any other file in this project, so we retire this file as a stub.
The original lemmas remain in git history for reference.