Hi Thierry,
Thank you for the proof: that made a really good learning material for
me!
I tried to understand what exactly R = ( ZZring ~QG ( ( RSpan ` ZZring
) ` { 5 } ) ) means: basically, ( RSpan ` ZZring ) ` { 5 } means 5ZZ, and
this defines a set whose elements are like <1, 6>, <1, 11>, <1, 16>, <2,
7>, <2, 12>...etc. When it comes to the goal, by df-ec, I starting knowing
it's saying ( R " { I ` 3 } ) = ( R " { 2 } ).
I haven't finished reading the proof and I'm in the stage of the
ZRHom, hope that I can finish it in a little time.
One more question somehow irrelevant: While I was jumping around
different pages of metamath, I found some of definitions (df-mulr) is like
.r = Slot 3, do you know what it means by Slot?
Bests
Kunhao
在2021年6月9日星期三 UTC+2 下午5:49:07<Thierry Arnoux> 写道：
> Hi again,
>
> Spoiler, I tried to do the proof, you can check the attachment if, but
> only if, you need some inspiration ;-)
> (I also wanted to be extra sure that my formalization was correct!)
> BR,
> _
> Thierry
>
> PS. Re-reading your original mail, I see you were looking for the base of
> ( Z/nZ ), the relevant theorem is ~znbas, which shows that the base you
> need is the quotient set.
>
>
> On 09/06/2021 23:07, Thierry Arnoux wrote:
>
> 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].
> 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
>
> <https://groups.google.com/d/msgid/metamath/2a25c673-3780-b43c-8ad2-15ccd04322dc%40gmx.net?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/35af315e-1735-4197-8c63-a091b758c389n%40googlegroups.com.
