Theorem spectralNorm_unique_field_norm_ext

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_field_norm_extView on Github →