Theorem PadicComplex.norm_eq_norm'

Modification history

2026-03-06 17:55
Mathlib/NumberTheory/Padics/Complex.lean
chore(Topology/Algebra/Valued/NormedValued): replace Valued.norm by Valuation.norm (#36284) …
Modified PadicComplex.norm_eq_norm'View on Github →
2026-03-05 11:23
Mathlib/NumberTheory/Padics/Complex.lean
fix(NumberTheory/Padics): remove diamond normed instance on C_p (#36118) …
Added PadicComplex.norm_eq_norm'View on Github →