Switch branches/tags
Nothing to show
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
..
Failed to load latest commit information.
.package
All.v
README.md
fps.v
frac.v
lemmas.v
padics.v
z_mod_p.v

README.md

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