Commit 2020-09-03 17:36 2d40d9c6

feat(data/padics): universal property of Z_p (#3950) We establish the universal property of $\mathbb{Z}_p$ as a projective limit. Given a family of compatible ring homs $f_k : R \to \mathbb{Z}/p^n\mathbb{Z}$, there is a unique limit $R \to \mathbb{Z}_p$. In addition, we:

• split padic_integers.lean into two files, creating ring_homs.lean
• renamings: padic_norm_z.* -> padic_int.norm_*