leadingCoeff_eq — Mathlib

English

The leading coefficient equals the coefficient at the order: leadingCoeff(x) = coeff(x, order(x)).

Русский

Ведущий коэффициент равен коэффициенту при порядке: leadingCoeff(x) = coeff(x, order(x)).

LaTeX

$$$ \\operatorname{leadingCoeff}(x) = \\operatorname{coeff}(x, x.\\mathrm{order}) $$$

Lean4

theorem leadingCoeff_eq {x : HahnSeries Γ R} : x.leadingCoeff = x.coeff x.order :=
  by
  by_cases h : x = 0
  · rw [h, leadingCoeff_zero, coeff_zero]
  · simp [leadingCoeff_of_ne_zero, orderTop_of_ne_zero, order_of_ne, h]

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