# Zulip Chat Archive

## Stream: maths

### Topic: isomorphism of rings of integers with different radices

#### Roman Bars (Feb 07 2021 at 17:48):

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 (Feb 07 2021 at 18:04):

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 (Feb 07 2021 at 18:04):

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

#### Mario Carneiro (Feb 07 2021 at 18:05):

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 (Feb 07 2021 at 18:08):

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 (Feb 07 2021 at 18:09):

in the case of binary, this is the `bit0`

and `bit1`

functions (on `nat`

), plus docs#nat.binary_rec

#### Bryan Gin-ge Chen (Feb 07 2021 at 18:21):

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 (Feb 08 2021 at 06:02):

@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 (Feb 08 2021 at 06:02):

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 (Feb 08 2021 at 06:03):

And there should be lemmas that show that `nat.of_digits`

behaves exactly the way it should with respect to addition, multiplication, etc...

Last updated: May 19 2021 at 02:10 UTC