constantCoeff_divXPowOrder — Mathlib

English

The constant coefficient of divXPowOrder f equals the coefficient at index order(f) in f.

Русский

Постоянный коэффициент divXPowOrder f равен коэффициенту при индексе order(f) в f.

LaTeX

$$$\operatorname{constantCoeff}(\operatorname{divXPowOrder} f) = \operatorname{coeff}_{\operatorname{order}(f)^{\text{toNat}}} f$$$

Lean4

theorem constantCoeff_divXPowOrder {f : R⟦X⟧} : constantCoeff (divXPowOrder f) = coeff f.order.toNat f := by
  simp [← coeff_zero_eq_constantCoeff]

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