Commit 2025-07-03 13:20 64499d3b

View on Github →

feat(Analysis.Normed.Unbundled.SpectralNormUnique): prove unique extension theorem (#26537) Let K be a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K be an algebraic extension. We show that the spectral norm on L is a nonarchimedean multiplicative norm, and any power-multiplicative K-algebra norm on L coincides with the spectral norm. More over, if L/K is finite, then L is a complete space. This result is [S. Bosch, U. Güntzer, R. Remmert,Non-Archimedean Analysis (Theorem 3.2.4/2)][bosch-guntzer-remmert].

Estimated changes

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

added def algNormFromConst

added theorem algNormFromConst_def

added theorem spectralAlgNorm_mul

added def spectralMulAlgNorm

added theorem spectralMulAlgNorm_def

added def spectralNorm.metricSpace

added def spectralNorm.normedAddCommGroup

added def spectralNorm.normedField

added def spectralNorm.normedSpace

added def spectralNorm.seminormedAddCommGroup

added def spectralNorm.uniformSpace

added theorem spectralNorm_unique

added theorem spectralNorm_unique_field_norm_ext