Commit 2025-05-27 21:58 74b10f15

feat(Analysis/Normed/Unbundled/SpectralNorm): add spectral norm (#23301) We define the spectral value and the spectral norm. We prove the norm extension theorem [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Theorem 3.2.1/2)][bosch-guntzer-remmert] : given a nonarchimedean normed field K and an algebraic extension L/K, the spectral norm is a power-multiplicative K-algebra norm on L extending the norm on K. All K-algebra automorphisms of L are isometries with respect to this norm. If L/K is finite, we get a formula relating the spectral norm on L with any other power-multiplicative norm on L extending the norm on K. As a prerequisite, we formalize the proof of [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Proposition 3.1.2/1)][bosch-guntzer-remmert].