isomorphism of rings of integers with different radices

Stream: maths

[Roman Bars]

So in Lean there is the standard definition of natural numbers as an inductive type with 0 and such as the constructors. We can also define binary natural numbers with 0, "append 0" and "append 1" as constructors and so on for any number of digits. To all of these types we can add negative numbers and make them into rings.

Can we formalize the idea that for any given number of digits all of these rings are isomorphic?

[Kevin Buzzard]

Yes, and I would imagine that all these things are done. There is pos_num and num in something like data.num.basic.

[Mario Carneiro]

For the case of binary natural numbers this is formalized as docs#num.to_nat_inj and similar theorems

[Mario Carneiro]

although it appears that the statement that num and nat are isomorphic as semirings is not explicitly stated, since it's a fairly low level file

[Mario Carneiro]

In general, however, rather than constructing a bunch of isomorphic types, I would prefer to see alternate constructors and recursors on nat that allow it to be viewed as binary natural numbers or ternary or phinary or what have you

[Mario Carneiro]

in the case of binary, this is the bit0 and bit1 functions (on nat), plus docs#nat.binary_rec

[Bryan Gin-ge Chen]

Along the lines of alternate constructors, there's also docs#nat.of_digits going from lists of natural numbers back to natural numbers.

[Johan Commelin]

@Roman Bars There is one technical downside to making all these new definitions. Even if you prove that nat is isomorphic to nat_in_base 5, if you prove a lemma about one of them, it isn't transparently automatically true for the other.

[Johan Commelin]

So the usual approach in formalisation is to build functions (like nat.of_digits that Bryan linked to above) that allow you to treat nat as if it were nat_in_base 5.

[Johan Commelin]

And there should be lemmas that show that nat.of_digits behaves exactly the way it should with respect to addition, multiplication, etc...