Theorems · Theorem · number theory

IsNonarchimedean.apply_sum_le

∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : AddCommMonoid β] [inst_1 : FunLike F β ℝ] [NonnegHomClass F β ℝ]
  [ZeroHomClass F β ℝ] {v : F} {l : α → β}, IsNonarchimedean ⇑v → ∀ {s : Finset α}, v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)

The ultrametric triangle inequality for finite sums.

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

2 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidFunLikeNonnegHomClassZeroHomClass