Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Abel's Limit Theorem

Email Gateway (Jan 23 2026 at 15:21):

From: Manuel Eberl <manuel@pruvisto.org>

Abel's Limit Theorem

by Kangfeng Ye

https://www.isa-afp.org/entries/Abel_Limit_Theorem.html

This entry mechanises Abel's limit theorem on power series with real
coefficients. The theorem also holds for complex numbers, but this entry
has not covered it yet. An application example of this theorem is also
presented in this entry to extend the generalised binomial theorem for a
specific example from (-1,1) to its boundary cases -1 and 1.

Enjoy!

Manuel

Last updated: Jan 31 2026 at 12:53 UTC