p-adic integers as inverse limit

Stream: Is there code for X?

[Adam Topaz]

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

[Kenny Lau]

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

[Adam Topaz]

Thanks

[Johan Commelin]

@Adam Topaz Feel free to review it

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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