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 条
  • [1] On approximation of p-adic numbers by p-adic algebraic numbers
    Beresnevich, VV
    Bernik, VI
    Kovalevskaya, EI
    JOURNAL OF NUMBER THEORY, 2005, 111 (01) : 33 - 56
  • [2] P-ADIC NUMBERS
    BARSKY, D
    CHRISTOL, G
    RECHERCHE, 1995, 26 (278): : 766 - 771
  • [3] P-ADIC NUMBERS IN PHYSICS
    BREKKE, L
    FREUND, PGO
    PHYSICS REPORTS-REVIEW SECTION OF PHYSICS LETTERS, 1993, 233 (01): : 1 - 66
  • [4] The frame of the p-adic numbers
    Avila, F.
    TOPOLOGY AND ITS APPLICATIONS, 2020, 273
  • [5] Simultaneous approximation problems of p-adic numbers and p-adic knapsack cryptosystems - Alice in p-adic numberland
    Inoue H.
    Kamada S.
    Naito K.
    P-Adic Numbers, Ultrametric Analysis, and Applications, 2016, 8 (4) : 312 - 324
  • [6] Geometry of P-adic numbers.
    Monna, AF
    PROCEEDINGS OF THE KONINKLIJKE NEDERLANDSE AKADEMIE VAN WETENSCHAPPEN, 1942, 45 (6/10): : 981 - 986
  • [7] Bernoulli numbers in p-adic analysis
    Kim, MS
    Son, JW
    APPLIED MATHEMATICS AND COMPUTATION, 2003, 146 (01) : 289 - 297
  • [8] P-ADIC ANALYSIS AND BERNOULLI NUMBERS
    BARSKY, D
    COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES SERIE A, 1976, 283 (16): : 1069 - 1072
  • [9] Relaxed algorithms for p-adic numbers
    Berthomieu, Jeremy
    van der Hoeven, Joris
    Lecerf, Gregoire
    JOURNAL DE THEORIE DES NOMBRES DE BORDEAUX, 2011, 23 (03): : 541 - 577
  • [10] Algebraic independence of p-adic numbers
    Nesterenko, Yu. V.
    IZVESTIYA MATHEMATICS, 2008, 72 (03) : 565 - 579
12345