Theorem spectralNorm_unique

Modification history

2025-07-03 13:20

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

feat(Analysis.Normed.Unbundled.SpectralNormUnique): prove unique extension theorem (#26537) …

Added spectralNorm_unique View on Github →