Thank you all for these suggestions! I think I'll be playing with the ( <" 2 1 2 1 "> _b 3 )= ; 70 and see how that will bring me.
Bests Kunhao 在2021年5月2日星期日 UTC+2 上午3:17:46<David A. Wheeler> 写道： > On May 1, 2021, at 10:01 AM, 'Alexander van der Vekens' via Metamath < > [email protected]> wrote: > > we would get ( <" 2 1 2 1 "> _b 3 )= ; 70, which seems to be a quite > good and natural representation. > > +1, I agree, that’s really clean. > > > That means > > _b = ( n e. Word ( 0 ..^ b ) , b e. NN |-> sum_ k e. dom n ( ( ( reverse > ` n ) ` k ) x. ( b ^ k ) ) ) > > That seems like a nice higher-level definition. > > I can easily imagine a number of general-purpose theorems building on this > notation. > > --- David A. Wheeler > > -- 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/72656920-4694-41ed-844f-daa146cff3dbn%40googlegroups.com.
