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_*`
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
