Commit 2026-03-19 16:26 308bf901

View on Github →

feat(RingTheory/Polynomial/GaussNorm): The gaussNorm is an absolute value if v is a nonarchimedean absolute value (#33736) We prove

Polynomial.gaussNorm_isAbsoluteValue {c : ℝ} {R : Type*} [Ring R] {v : AbsoluteValue R ℝ}
  (hna : IsNonarchimedean v) (hc : 0 < c) : IsAbsoluteValue (gaussNorm v c)

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

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

added theorem IsNonarchimedean.apply_sum_eq_of_lt

Modified Mathlib/RingTheory/Polynomial/GaussNorm.lean

modified theorem Polynomial.exists_eq_gaussNorm

added theorem Polynomial.exists_min_eq_gaussNorm

modified theorem Polynomial.gaussNorm_C

modified theorem Polynomial.gaussNorm_coe_powerSeries

modified theorem Polynomial.gaussNorm_eq_zero_iff

added theorem Polynomial.gaussNorm_isAbsoluteValue

modified theorem Polynomial.gaussNorm_monomial

added theorem Polynomial.gaussNorm_mul

added theorem Polynomial.gaussNorm_mul_le

modified theorem Polynomial.gaussNorm_nonneg

added theorem Polynomial.gaussNorm_zero_right

added theorem Polynomial.isNonarchimedean_gaussNorm

modified theorem Polynomial.le_gaussNorm