The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.
CITATION STYLE
Pelayo, Á., Voevodsky, V., & Warren, M. A. (2015). A univalent formalization of the p-adic numbers. Mathematical Structures in Computer Science, 25(5), 1147–1171. https://doi.org/10.1017/S0960129514000541
Mendeley helps you to discover research relevant for your work.