Theorem spectralValue_le_one_iff

Modification history

2025-10-14 10:22

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

feat(Analysis/Normed/Unbundled/SpectralNorm): add API (#26668)

Added spectralValue_le_one_iff View on Github →