addVal_apply_of_ne — Mathlib

English

If x ≠ 0, then addVal x = x.order, i.e., the valuation picks the actual order when nonzero.

Русский

Если x ≠ 0, то addVal x = x.order, то есть оценка выбирает фактический порядок для ненулевой серии.

LaTeX

$$addVal Γ R x = x.order (при x ≠ 0)$$

Lean4

@[simp]
theorem addVal_apply_of_ne {x : HahnSeries Γ R} (hx : x ≠ 0) : addVal Γ R x = x.order :=
  addVal_apply.trans (order_eq_orderTop_of_ne_zero hx).symm

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