[isabelle] inverse definition in modulo p



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.