coeff_untop_eq_leadingCoeff — Mathlib

English

For x ≠ 0, the coefficient at the top index after removing the top equals the leading coefficient.

Русский

Для x ≠ 0 коэффициент при ведущем показателе после удаления верхнего равен ведущему коэффициенту.

LaTeX

$$$ x \\neq 0 \\Rightarrow x.\\operatorname{coeff}(x.\\operatorname{orderTop}.untop(\\operatorname{orderTop\\_ne\\_top}(x))) = \\operatorname{leadingCoeff}(x) $$$

Lean4

theorem coeff_untop_eq_leadingCoeff {x : HahnSeries Γ R} (hx) : x.coeff (x.orderTop.untop hx) = x.leadingCoeff :=
  by
  rw [orderTop_ne_top] at hx
  rw [leadingCoeff_of_ne_zero hx, (WithTop.untop_eq_iff _).mpr (orderTop_of_ne_zero hx)]

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