# 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:
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 at rbg.informatik.tu-darmstadt.de 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
thanks

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