In Mathlib, the $p$-adic numbers given a prime $p$ were defined in terms of completion, i.e. $\mathbb Q_p$ as the ring of Cauchy sequences over $\mathbb Q$ with respect to the $p$-adic metric modulo its maximal ideal of null sequences. Then $\mathbb Z_p$ was taken as ${x \in \mathbb Q_p | |x|_p \leq 1}$.
In this project, we define $\mathbb Z_p \coloneqq \varprojlim_n \mathbb Z / p^n$ and derive its basic properties as a ring.
