addVal_apply — Mathlib

English

For HahnSeries, addVal equals the orderTop, i.e., the additive valuation returns the smallest index with nonzero coefficient, or ⊤ for zero.

Русский

Для HahnSeries корректно: addVal x = orderTop, т.е. минимальный индекс с ненулевым коэффициентом или ⊤ для нуля.

LaTeX

$$addVal Γ R x = x.orderTop$$

Lean4

theorem addVal_apply {x : HahnSeries Γ R} : addVal Γ R x = x.orderTop :=
  AddValuation.of_apply _

Похожие утверждения