addVal_le_of_coeff_ne_zero — Mathlib

English

Let Γ be a linearly ordered cancellative additive monoid and R a domain. For any Hahn series x ∈ HahnSeries(Γ, R) and any g ∈ Γ, if the coefficient of x at g is nonzero, then the Hahn valuation of x satisfies addVal(Γ, R)(x) ≤ g.

Русский

Пусть Γ — упорядоченный по линейному порядку отменимый добавочный моноид, R — домен. Для любого ряда Хана x ∈ HahnSeries(Γ, R) и любого g ∈ Γ, если коэффициент x по g не равен нулю, то добавочная оценка x удовлетворяет addVal(Γ, R)(x) ≤ g.

LaTeX

$$$\text{If } x \in \mathrm{HahnSeries}(\Gamma, R) \text{ and } g \in \Gamma \text{ with } x_{g} \neq 0, \\ addVal(\Gamma, R)(x) \le g.$$$

Lean4

theorem addVal_le_of_coeff_ne_zero {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) : addVal Γ R x ≤ g :=
  orderTop_le_of_coeff_ne_zero h

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