Theorem PadicComplex.norm_def

Modification history

2026-03-05 11:23

Mathlib/NumberTheory/Padics/Complex.lean

fix(NumberTheory/Padics): remove diamond normed instance on C_p (#36118) …

Deleted PadicComplex.norm_def View on Github →

2025-07-07 13:51

Mathlib/NumberTheory/Padics/Complex.lean

feat(NumberTheory/Padics/Complex.lean): add the padic complex numbers (#26675) …

Added PadicComplex.norm_def View on Github →