Theorem spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow

Modification history

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