Hi Kunhao, in addition to the answers you already got about the representation, in case you don't already know about
http://us.metamath.org/mpegif/df-dig.html in Alexander's mathbox: "Definition of an operation to obtain the k_th digit of a nonnegative real number in the positional system with base b. k=-1 corresponds to the first digit of the fractional part" I don't know if Alexander has also done some work on an "efficient" way for generic base representations. Glauco Il giorno venerdì 23 aprile 2021 alle 15:29:37 UTC+2 [email protected] ha scritto: > Hello all! > I'm quite a beginner on metamath. Recently I search on representing > numbers in base other than 10, like in base 3 or base 7 when I formalize > some exercises in number theory. For example, I want to write > 2121_3 - 212_3 (both in base 3). > > I browse through the Th.List on the website and it seems that I didn't > find relevant information. Any hint is welcome! > > Bests Regards > Kunhao > -- 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/97d5a396-cbb6-4844-a035-ba7a6361e7fan%40googlegroups.com.
