p-adic numbers

Formalization of p-adic numbers, described in

Álvaro Pelayo, Vladimir Voevodsky, and Michael A. Warren A univalent formalization of the p-adic numbers Math. Struct. in Comp. Science (2015), vol. 25, pp. 1147–1171. doi:10.1017/S0960129514000541

Also see Álvaro Pelayo, Vladimir Voevodsky and Michael A. Warren, A preliminary univalent formalization of the p-adic numbers at arXiv.

Contents (alphabetic order of files)

• fps.v — formal power series, only based on lemmas.v
• frac.v — fractions, only based on lemmas.v
• lemmas.v — preparations, needed for all other files
• padics.v — the p-adic numbers, needs all other files
• z_mod_p.v — integers mod p, only based on lemmas.v