coeff_of_lt_order — Mathlib

English

If degree d is strictly less than the order of f, then coeff d f = 0.

Русский

Если deg d < order(f), то coeff d f = 0.

LaTeX

$$degree d < f.order → coeff d f = 0$$

Lean4

/-- The `n`th coefficient of a formal power series is `0` if `n` is strictly
smaller than the order of the power series. -/
theorem coeff_of_lt_order {d : σ →₀ ℕ} (h : degree d < f.order) : coeff d f = 0 :=
  by
  rw [degree_eq_weight_one] at h
  exact coeff_eq_zero_of_lt_weightedOrder _ h

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