Zulip Chat Archive

Stream: Is there code for X?

Topic: p-adic integers as inverse limit


view this post on Zulip Adam Topaz (Sep 02 2020 at 14:03):

Does mathlib have the fact that Zp=limnZ/pn\mathbf{Z}_p = \lim_n \mathbf{Z}/p^n?

view this post on Zulip Kenny Lau (Sep 02 2020 at 14:11):

https://github.com/leanprover-community/mathlib/pull/3950/files#diff-3efee1ad50bc208912292df6de31b124R615

view this post on Zulip Adam Topaz (Sep 02 2020 at 14:13):

Thanks

view this post on Zulip Johan Commelin (Sep 02 2020 at 14:29):

@Adam Topaz Feel free to review it

view this post on Zulip Johan Commelin (Sep 02 2020 at 14:29):

We sort of need to rely on external reviewers, since I'm the author.

view this post on Zulip Johan Commelin (Sep 02 2020 at 14:29):

So if you or @Kenny Lau could help, that would be great

view this post on Zulip Johan Commelin (Sep 02 2020 at 14:30):

Then other maintainers can kick it on the queue (-;


Last updated: May 17 2021 at 15:13 UTC