Hello all,
Currently, I am stuck on formalization some exercise of number theory
involving the multiplication inverse in Z/nZ. Like, compute 3^{-1} in Z/5Z,
which gives 2 (because 6 mod 5 = 1).
It's easy to translate them into the relation of modulo. For example
cheating like
|- ( ph -> X e. NN0 )
|- ( ph-> ( ( X x. 3 ) mod 5 ) = 1 )
|- ( ph -> ( X mod 5 ) = 2 )
However, I want to know if I can directly provide the information of
inverse, my attempt is something like
|- R = ( CCfld |` ( Z/nZ ` 5 ) )
|- I = ( invr ` R )
|- ( ph -> ( I ` 3 ) = 2 )
Since the best way to test if a formalization is correct or not is trying
to prove it, I tried but I failed, and I struggle a lot in providing extra
def like "B = ( Base ` R )". Do you have any suggestion on the
formalization? Thank you a lot!
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/5e9d1415-8e81-493d-9a93-5d04edb4a1d9n%40googlegroups.com.
