Theorem PadicAlgCl.spectralNorm_eq

Modification history

2025-07-07 13:51
Mathlib/NumberTheory/Padics/Complex.lean
feat(NumberTheory/Padics/Complex.lean): add the padic complex numbers (#26675) …
Added PadicAlgCl.spectralNorm_eqView on Github →