coeff_orderTop_ne — Mathlib

English

If x.orderTop = some g, then x.coeff g ≠ 0.

Русский

Если orderTop x = some g, то x.coeff g ≠ 0.

LaTeX

$$x.orderTop = \mathrm{WithTop}.some g \Rightarrow x.coeff g \neq 0$$

Lean4

theorem coeff_orderTop_ne {x : HahnSeries Γ R} {g : Γ} (hg : x.orderTop = g) : x.coeff g ≠ 0 :=
  by
  have h : orderTop x ≠ ⊤ := by simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]
  have hx : x ≠ 0 := orderTop_ne_top.1 h
  rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hg
  rw [← hg]
  exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

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