Theorems · Theorem · number theory

IsNonarchimedean.apply_sum_univ_le

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

The ultrametric triangle inequality for finite sums.

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidFunLikeNonnegHomClassZeroHomClassFintype