Theorem spectralAlgNorm_of_finiteDimensional_normal_def

Modification history

2025-05-27 21:58
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
feat(Analysis/Normed/Unbundled/SpectralNorm): add spectral norm (#23301) …
Added spectralAlgNorm_of_finiteDimensional_normal_defView on Github →