Mathlib v3 is deprecated. Go to Mathlib v4

Def padic_norm_z

Modification history

2020-05-31 17:05

src/data/padics/padic_integers.lean

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

Deleted padic_norm_z View on Github →

2018-10-02 14:08

data/padics/padic_integers.lean

feat(data/padics): use prime typeclass

Modified padic_norm_z View on Github →

2018-10-02 14:02

data/padics/padic_integers.lean

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

Added padic_norm_z View on Github →