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/E2576913-AAD6-45B1-88D7-C841BB3C6D5B%40dwheeler.com.
