Theorem spectralNorm.spectralMulAlgNorm_eq_of_mem_roots

Modification history

2025-10-14 10:22
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
feat(Analysis/Normed/Unbundled/SpectralNorm): add API (#26668)
Added spectralNorm.spectralMulAlgNorm_eq_of_mem_rootsView on Github →