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 <mail@andreas-lochbihler.de>
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].

[1]
https://s3.amazonaws.com/aops-cdn.artofproblemsolving.com/resources/articles/lifting-the-exponent.pdf

Andreas


Last updated: Sep 25 2021 at 09:17 UTC