This is an unofficial reimagining of the Archive of Formal Proofs
Hensel's Lemma for the p-adic Integersby Aaron Crighton