Re: [isabelle] inverse definition in modulo p

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:

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 at wrote:
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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.