Mathlib v3 is deprecated. Go to Mathlib v4

Theorem padic.zero_def

Modification history

2022-10-04 18:24

src/number_theory/padics/padic_numbers.lean

feat(number_theory/padic_numbers): bundle padic_norm_e (#16650) …

Added padic.zero_def View on Github →