Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Kummer's congruence


view this post on Zulip Email Gateway (Mar 29 2024 at 12:48):

From: Lawrence Paulson <lp15@cam.ac.uk>
We have yet another contribution from the ever-busy Manuel Eberl: Kummer's congruence. Here’s a summary of the abstract (omitting the mathematical formulas):

This entry provides proofs for two important congruences involving Bernoulli numbers. The proofs follow Cohen's textbook Number Theory Volume II: Analytic and Modern Tools. The first result that I showed is Voronoi's congruence. Building upon this, I then derive Kummer's congruence. One application of these congruences is to prove that there are infinitely many irregular primes, which I formalised as well.

Now online at https://www.isa-afp.org/entries/Kummer_Congruence.html

Larry Paulson


Last updated: May 04 2024 at 20:16 UTC