order_le_of_coeff_ne_zero — Mathlib

English

If the coefficient at g is nonzero, then the order of x is ≤ g.

Русский

Если коэффициент при $g$ не равен нулю, то порядок $x$ не превосходит $g$.

LaTeX

$$$ x.\\operatorname{coeff}(g) \\neq 0 \\Rightarrow \\operatorname{order}(x) \\le g $$$

Lean4

theorem order_le_of_coeff_ne_zero {Γ} [Zero Γ] [LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) :
    x.order ≤ g :=
  le_trans (le_of_eq (order_of_ne (ne_zero_of_coeff_ne_zero h))) (Set.IsWF.min_le _ _ ((mem_support _ _).2 h))

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