Commit 2025-07-24 23:59 962b2468

View on Github →

feat(Analysis): Spectral norm is nontrivial (#27448) From the 2025 Local Class Field Theory Workshop.

Estimated changes

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

added def spectralNorm.nontriviallyNormedField