[isabelle-dev] Sum_of_powers

[Manuel Eberl]

It already is in the AFP: 
https://www.isa-afp.org/theories/bernoulli/#Bernoulli

If I recall correctly, I took Lukas's theory from HOL-ex, added a lot of 
my own stuff, and put it in the AFP (with his permission and with him as 
a co-author).

As for why I did not delete the version in HOL-ex, I cannot remember – 
perhaps because it still is a small and self-contained derivation of 
that result.

Manuel


On 15/08/2022 15:31, Lawrence Paulson wrote:
> I think that HOL/ex/Sum_of_Powers.thy should be moved to the AFP.
>
> It is a significant result: that the sum of the K-th powers of the first N positive integers is a polynomial in N. Using Bernoulli numbers and Bernoulli polynomials. This should not be hidden away in HOL-ex
>
> Larry
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev