Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Lifting the Exponent

view this post on Zulip Email Gateway (May 31 2021 at 18:41):

From: Andreas Lochbihler <>
I'm happy to announce a new small entry in the AFP:

Lifting the Exponent by Jakub Kądziołka

Abstract: We formalize the Lifting the Exponent Lemma, which shows how to find the largest
power of p dividing a^n ± b^n, for a prime p and positive integers a and b. The proof
follows [1].



Last updated: Jul 15 2022 at 23:21 UTC