
@Book{dummit2004abstract,
 author = {Dummit, David},
 title = {Abstract algebra},
 publisher = {John Wiley \& Sons, Inc},
 year = {2004},
 address = {Hoboken, NJ},
 isbn = {0471433349}
 }

@Book{engler2005valued,
 author = {Engler, Antonio},
 title = {Valued fields},
 publisher = {Springer},
 year = {2005},
 address = {Berlin New York},
 isbn = {354024221X}
 }

@misc{keithconrad, title={Hensel's Lemma}, url={https://kconrad.math.uconn.edu/blurbs/gradnumthy/hensel.pdf}, author={Conrad, Keith}} 

@inproceedings{Thi,
author = {Lewis, Robert Y.},
title = {A Formal Proof of Hensel's Lemma over the p-Adic Integers},
year = {2019},
isbn = {9781450362221},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3293880.3294089},
doi = {10.1145/3293880.3294089},
abstract = {The field of p-adic numbers ℚp and the ring of p-adic integers ℤp are essential constructions of modern number theory. Hensel’s lemma, described by Gouv\^{e}a as the “most important algebraic property of the p-adic numbers,” shows the existence of roots of polynomials over ℤp provided an initial seed point. The theorem can be proved for the p-adics with significantly weaker hypotheses than for general rings. We construct ℚp and ℤp in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensel’s lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic.},
booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {15–26},
numpages = {12},
keywords = {Hensel's lemma, formal proof, Lean, p-adic},
location = {Cascais, Portugal},
series = {CPP 2019}
}

@article{10.2307/2274477,
 ISSN = {00224812},
 URL = {http://www.jstor.org/stable/2274477},
 author = {Johan Pas},
 journal = {The Journal of Symbolic Logic},
 number = {3},
 pages = {1125--1129},
 publisher = {Association for Symbolic Logic},
 title = {On the Angular Component Map Modulo P},
 volume = {55},
 year = {1990}
}

@article{denef1986,
author = {Denef, Jan},
journal = {Journal für die reine und angewandte Mathematik},
keywords = {rationality of Poincaré series; Macintyre's theorem; elimination of quantifiers; p-adic fields; cell decomposition theorem},
pages = {154-166},
title = {p-adic Semi-Algebraic Sets and Cell Decomposition.},
url = {http://eudml.org/doc/152854},
volume = {369},
year = {1986},
}
