Mathlib v3 is deprecated. Go to Mathlib v4

Def padic_int.add

Modification history

2020-05-31 17:05

src/data/padics/padic_integers.lean

chore(*): update to lean 3.15.0 (#2851) …

Deleted padic_int.add View on Github →

2018-10-02 14:08

data/padics/padic_integers.lean

feat(data/padics): use prime typeclass

Modified padic_int.add View on Github →

2018-08-16 11:23

data/padics/padic_integers.lean

feat(data/padics): p-adic numbers (#262)

Added padic_int.add View on Github →