Def spectralNorm.nontriviallyNormedField

Modification history

2026-04-19 00:33
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
chore: adaptations for overlapping instances linter (#38151) …
Modified spectralNorm.nontriviallyNormedFieldView on Github →
2025-07-24 23:59
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
feat(Analysis): Spectral norm is nontrivial (#27448) …
Added spectralNorm.nontriviallyNormedFieldView on Github →