Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: Partial Fraction Expansion of ...


view this post on Zulip Email Gateway (Mar 16 2022 at 11:44):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new entry by Manuel Eberl:

A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent

In this article, I formalise a proof from THE BOOK; namely a formula that was called ‘one of the most beautiful formulas involving elementary functions’. The proof uses Herglotz's trick to show the real case and analytic continuation for the complex case.

It is small, but perfectly formed. Now online at https://www.isa-afp.org/entries/Cotangent_PFD_Formula.html

Larry


Last updated: Apr 19 2024 at 08:19 UTC