coeff_eq_zero_of_lt_orderTop — Mathlib

English

If i is less than orderTop(x), then the i-th coefficient of x is zero.

Русский

Если i < orderTop(x), то коэффициент x на i равен нулю.

LaTeX

$$$i < x.orderTop \\Rightarrow x.coeff i = 0$$$

Lean4

theorem coeff_eq_zero_of_lt_orderTop {x : HahnSeries Γ R} {i : Γ} (hi : i < x.orderTop) : x.coeff i = 0 :=
  by
  rcases eq_or_ne x 0 with (rfl | hx)
  · exact coeff_zero
  contrapose! hi
  rw [← mem_support] at hi
  rw [orderTop_of_ne_zero hx, WithTop.coe_lt_coe]
  exact Set.IsWF.not_lt_min _ _ hi

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