A univalent formalization of the p-adic numbers

被引：10
|
作者：
Pelayo, Alvaro [1 ,2 ]
Voevodsky, Vladimir [2 ]
Warren, Michael A.
机构：
[1] Univ Calif San Diego, Dept Math, La Jolla, CA 92093 USA
[2] Inst Adv Study, Sch Math, Princeton, NJ 08540 USA
来源：
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | 2015年 / 25卷 / 05期
基金：
美国国家科学基金会;
关键词：
CONVEXITY;
D O I：
10.1017/S0960129514000541
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：1147 / 1171
页数：25
相关论文
共 50 条
  • [21] Quantum mechanics on p-adic numbers
    Vourdas, A.
    JOURNAL OF PHYSICS A-MATHEMATICAL AND THEORETICAL, 2008, 41 (45)
  • [22] ON EXPRESSIBLE SETS AND p-ADIC NUMBERS
    Hancl, Jaroslav
    Nair, Radhakrishnan
    Pulcerova, Simona
    Sustek, Jan
    PROCEEDINGS OF THE EDINBURGH MATHEMATICAL SOCIETY, 2011, 54 : 411 - 422
  • [23] Approximation lattices of p-adic numbers
    deSmedt, S
    P-ADIC FUNCTIONAL ANALYSIS, 1997, 192 : 375 - 382
  • [24] On p-adic T-numbers
    Pejkovic, Tomislav
    PUBLICATIONES MATHEMATICAE-DEBRECEN, 2013, 82 (3-4): : 549 - 567
  • [25] P ≠ NC over the p-adic numbers
    Maller, M
    Whitehead, J
    JOURNAL OF COMPLEXITY, 2003, 19 (02) : 125 - 131
  • [26] A derivative on the field of p-adic numbers
    Avdispahić M.
    Memić N.
    P-Adic Numbers, Ultrametric Analysis, and Applications, 2010, 2 (4) : 278 - 284
  • [27] On the heights of totally p-adic numbers
    Fili, Paul
    JOURNAL DE THEORIE DES NOMBRES DE BORDEAUX, 2014, 26 (01): : 103 - 109
  • [28] The p-adic law of large numbers
    Zelenov, E. I.
    IZVESTIYA MATHEMATICS, 2016, 80 (03) : 489 - 499
  • [29] BERNOULLI NUMBERS AND L P-ADIC FUNCTIONS
    FRESNEL, J
    ANNALES DE L INSTITUT FOURIER, 1967, 17 (02) : 281 - &
  • [30] On probability distributions on the field of p-adic numbers
    Khrennikov, AY
    THEORY OF PROBABILITY AND ITS APPLICATIONS, 1996, 40 (01) : 159 - 162
12345