Indexed metadata
A univalent formalization of the p -adic numbers
ÁLVARO PELAYO, VLADIMIR VOEVODSKY, MICHAEL A. WARREN
Source record
Source: Crossref
Published: Feb 13, 2015
DOI: 10.1017/s0960129514000541
Open original source ↗Source abstract
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.
Evidence graph
No public relationships recorded yet.
Integrity note: This page is a factual metadata record created by deterministic ingestion. It is not a claim that the work moves a mathematical frontier or has been independently verified.