A formal proof of hensel's lemma over the p-adic integers

Robert Y. Lewis. A formal proof of hensel's lemma over the p-adic integers. In Assia Mahboubi, Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. pages 15-26, ACM, 2019. [doi]

@inproceedings{Lewis19-0,
  title = {A formal proof of hensel's lemma over the p-adic integers},
  author = {Robert Y. Lewis},
  year = {2019},
  doi = {10.1145/3293880.3294089},
  url = {https://doi.org/10.1145/3293880.3294089},
  researchr = {https://researchr.org/publication/Lewis19-0},
  cites = {0},
  citedby = {0},
  pages = {15-26},
  booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019},
  editor = {Assia Mahboubi and Magnus O. Myreen},
  publisher = {ACM},
  isbn = {978-1-4503-6222-1},
}