Def algNormFromConst

Modification history

2026-09-01 11:45
Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean
refactor(Analysis/Normed/Unbundled/SpectralNorm): extract, generalize, and golf `algNormFromConst` (#43019) …
Modified algNormFromConstView on Github →
2026-08-21 16:38
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
chore(Analysis/Normed/Unbundled/SeminormFromConst): remove unnecessary hypothesis (#43022) …
Modified algNormFromConstView on Github →
2025-07-03 13:20
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
feat(Analysis.Normed.Unbundled.SpectralNormUnique): prove unique extension theorem (#26537) …
Added algNormFromConstView on Github →