Def spectralNorm.normedAddCommGroup

Modification history

2025-10-14 10:22

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

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

Modified spectralNorm.normedAddCommGroup View on Github →

2025-07-03 13:20

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

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

Added spectralNorm.normedAddCommGroup View on Github →