Sorry for the duplicate post. I deleted the original to edit a detail that FL didn't want publicly exposed. (In Aug. 2020, Google Groups removed the ability to edit posts.)
-------- Forwarded Message -------- Subject: Positional representation Date: Sat, 24 Apr 2021 13:25:26 +0200 (CEST) From: FL 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e5394ab5-03ba-42e5-8970-3e3bcbb6cb0fn%40googlegroups.com.
