leadingCoeff_of_ne_zero — Mathlib

English

For x ≠ 0, the leading coefficient equals the coefficient at the leading exponent.

Русский

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

LaTeX

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

Lean4

theorem leadingCoeff_of_ne_zero {x : HahnSeries Γ R} (hx : x ≠ 0) :
    x.leadingCoeff = x.coeff (x.orderTop.untop <| orderTop_ne_top.2 hx) := by simp [leadingCoeff, orderTop, hx]

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