Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] inverse definition in modulo p

view this post on Zulip Email Gateway (Aug 18 2022 at 09:48):

From: kuecuek@rbg.informatik.tu-darmstadt.de
Hallo everbody,

is there any definition about the inverse of a number in modulo another
number?

for Example

inv x p =y ==> y*x =1 mod p

thanks

view this post on Zulip Email Gateway (Aug 18 2022 at 09:48):

From: Jeremy Avigad <avigad@cmu.edu>
There is a function

MultInv p x

which returns a multiplicative inverse modulo a prime p, defined in the
file Int2 in the NumberTheory directory.

There is a more extensive number theory library here:

http://www.andrew.cmu.edu/user/avigad/isabelle/

but the files are not very cleaned and polished, and they haven't been
updated from Isabelle 2004.

I am in the process of revising the number theory library from the
bottom up, but I have not gotten very far with this. I do have better
and more algebraic treatments of unique factorization and residue rings,
though they too are incomplete. I can send you the files if you're
interested.

Best wishes,

Jeremy Avigad

kuecuek@rbg.informatik.tu-darmstadt.de wrote:

Last updated: May 03 2024 at 04:19 UTC