Theorem PadicComplex.norm_extends'

Modification history

2026-03-05 11:23
Mathlib/NumberTheory/Padics/Complex.lean
fix(NumberTheory/Padics): remove diamond normed instance on C_p (#36118) …
Added PadicComplex.norm_extends'View on Github →