Hi Kunhao,
As stated by `zncrng`, ( Z/nZ `5 ) is already the ring itself, so you
can work within the ring Y = ( Z/nZ `5 ), and with its multiplicative
inverse operation I = ( invr ` Y ).
The elements of that ring are not exactly the integers, they are
equivalence classes, so your final statement will rather look like
( I ` [ 3 ] R ) = [ 2 ] R
Where R is the underlying equivalence relation.
I hope this puts you on the track!
BR,
_
Thierry
On 09/06/2021 18:53, Kunhao Zheng wrote:
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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/5e9d1415-8e81-493d-9a93-5d04edb4a1d9n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/5e9d1415-8e81-493d-9a93-5d04edb4a1d9n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/2a25c673-3780-b43c-8ad2-15ccd04322dc%40gmx.net.
