Commit 2026-06-17 10:37 69892ec2

View on Github →

feat: lemmas towards showing gaussNorm on MvPowerSeries is an absolute value (#38049) We prove lemmas: gaussNorm_mul_le and gaussNorm_le_mul which will allow us to show it is an absolute value on Mv restricted power series.

Estimated changes

Modified Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean

added theorem IsNonarchimedean.add_eq_max_of_ne'

modified theorem IsNonarchimedean.apply_sum_eq_of_lt

modified theorem IsNonarchimedean.finset_image_add

modified theorem IsNonarchimedean.finset_image_add_of_nonempty

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

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

Modified Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean

added theorem MvPowerSeries.Finset.Nonempty.map_sum_le_sup'_map

added theorem MvPowerSeries.antidiagonal_dominant

added theorem MvPowerSeries.gaussNorm_le_mul

added theorem MvPowerSeries.gaussNorm_mul_le

added theorem MvPowerSeries.ultrametric_strict

Modified Mathlib/RingTheory/Polynomial/GaussNorm.lean