I also want to mention that Jim Kingdon's suggestion of simply using ((3 · ((3 · 2) + 1)) + 2) has official support in set.mm, in that for every dec* theorem there is a corresponding num* theorem about the generalized base representation of numbers. As Norm says, this suite of theorems was used when I was working in base 4, but they are not hard coded to any particular base, unlike df-dec which is base-10 specific.
> To represent numbers in any basis, we can also use finite sequences of figures (aka words) and implement the operations accordingly. It has the advantage that we can make collections of numbers represented by position, what is not allowed by Mario Carneiro's denotation. Another variation on this that has come up in lean is to use the base X and form a polynomial instead of a number. However you can't do carrying with this representation, because it is base-dependent, so you have to live with non-canonical representations of numbers like X*1 + 13 with X = 10. > (The same representation duality exists for fractions and should also be implemented, since it is the only way to implement concepts like that of irreductible fractions.) It's possible to talk about irreducible fractions without an actual representation like this - you can simply have a hypothesis a is coprime to b and then talk about some property of a/b. > P.S. Does anyone know what is going on at Lean. Why did they have to change the concept of monoid? Monoids have recently been changed to incorporate the monoid power operation into the structure, even though it is formally redundant, in order to solve some definitional equality issues that metamath does not have to deal with because it is based on ZFC. On Sat, Apr 24, 2021 at 6:27 PM Norman Megill <[email protected]> wrote: > FL asked me to post this for him. > > -------- Forwarded Message -------- > Subject: Positional representation > Date: Sat, 24 Apr 2021 13:25:26 +0200 (CEST) > From: frederic.line > To: Megill Norman > > Hi Norm, > > can you post this mail: > > To represent numbers in any basis, we can also use finite sequences of > figures (aka words) and implement the operations > accordingly. It has the advantage that we can make collections of numbers > represented by position, > what is not allowed by Mario Carneiro's denotation. > > (The same representation duality exists for fractions and should also be > implemented, since it is the only > way to implement concepts like that of irreductible fractions.) > > P.S. Does anyone know what is going on at Lean. Why did they have to > change the concept of monoid? > > -- > FL > > -- > 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/10bcbe8b-ed80-407b-b965-7614752e8b21n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/10bcbe8b-ed80-407b-b965-7614752e8b21n%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/CAFXXJSu%2B_-ggpBYoMyATUBf3ArpiVF9d8azaci3eo4rXzR8Axg%40mail.gmail.com.
