coeff_divXPowOrder — Mathlib

English

For any f ∈ R[[X]] and n ∈ ℕ, the nth coefficient of divXPowOrder f equals the coefficient of index n+order(f) in f.

Русский

Для любого f ∈ R[[X]] и n ∈ ℕ, коэффициент n у divXPowOrder f равен коэффициентy при n+order(f) у f.

LaTeX

$$$\operatorname{coeff}_n(\operatorname{divXPowOrder} f) = \operatorname{coeff}_{n + \operatorname{order}(f)} f$$$

Lean4

@[simp]
theorem coeff_divXPowOrder {f : R⟦X⟧} {n : ℕ} : coeff n (divXPowOrder f) = coeff (n + f.order.toNat) f :=
  coeff_mk _ _

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