Mathlib v3 is deprecated. Go to Mathlib v4

Theorem padic_int.val_eq_coe

Modification history

2020-05-31 17:05

src/data/padics/padic_integers.lean

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

Modified padic_int.val_eq_coe View on Github →

2018-10-02 14:08

data/padics/padic_integers.lean

feat(data/padics): use prime typeclass

Modified padic_int.val_eq_coe View on Github →

2018-10-02 14:02

data/padics/padic_integers.lean

feat(data/padics): use has_norm typeclasses for padics

Added padic_int.val_eq_coe View on Github →