Commit 2025-03-04 17:12 1199129f

View on Github →

feat(Analysis.Normed.Ring.FiniteExtension): prove existence of nonarchimedean power multiplicative norm on finite extension (#22081) We prove [BGR, Lemma 3.2.1./3][bosch-guntzer-remmert] : if K is a normed field with a nonarchimedean power-multiplicative norm and L/K is a finite extension, then there exists at least one power-multiplicative K-algebra norm on L extending the norm on K.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Ring/FiniteExtension.lean

added def Basis.norm

added theorem Basis.norm_extends

added theorem Basis.norm_isNonarchimedean

added theorem Basis.norm_mul_le_const_mul_norm

added theorem Basis.norm_repr_le_norm

added theorem Basis.norm_smul

added theorem exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

added theorem Basis.repr_smul'