[Question of Formalization & Proof] Inverse in number theory

[Kunhao Zheng]

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!

[Thierry Arnoux]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5e9d1415-8e81-493d-9a93-5d04edb4a1d9n%40googlegroups.com.

[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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2a25c673-3780-b43c-8ad2-15ccd04322dc%40gmx.net.

[Kunhao Zheng]

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

[Mario Carneiro]

On Mon, Jun 14, 2021 at 3:43 AM Kunhao Zheng <dye...@gmail.com> wrote:

    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?

That has to do with the encoding of structures. "Slot N" defines a function whose action is like ( .r ` S ) = ( S ` 3 ), that is, .r acts on structures, viewed as functions, to extract the element labelled "3". This is then paired with the ndx "structure", which is just the identity function, so that ( .r ` ndx ) = ( ndx ` 3 ) = 3, so you will usually see ( .r ` ndx ) used instead of 3 (because we want to encapsulate the actual integer being used here). Finally, a concrete structure will have something like

MyRing = { <. 1 , B >. , <. 2 , + >. , <. 3 , * >. }

which defines a finite function with value "B" at 1, "+" at 2 and "*" at 3. In order to make it more clear which component is which we use that ndx trick:

MyRing = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , * >. }

 

and now when you write ( .r ` MyRing ) it evaluates to ( MyRing ` 3 ) which is *. So this is all just to extract the ring multiplication operation from a structure which specifies what the base set, addition, and multiplication of that structure is. The class "Ring" is the collection of all structures whose addition and multiplication operations extracted in this way adhere to the ring axioms, so we would have a theorem like "MyRing e. Ring" and then use it together with lemmas like "( .r ` MyRing ) = * " to apply ring theorems.

Mario

[Thierry Arnoux]

Hi Kunhao,

Now that you have a mathbox, feel free to add to it this theorem (or
maybe a more general version of it), it you feel like it!

set.mm also has the operation ` mod ` (see ~ df-mod), and I'm sure there
is an easier and more natural way to describe that ` R ` relation using
` mod `, probably something around the lines of ` M R N <-> ( M mod 5 )
= ( N mod 5 ) ` for M, N in ZZ.

BR,
_
Thierry