coeff_eq_zero_of_lt_weightedOrder

English

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

Русский

Если вес w d строго меньше взвешенного порядка f, то coeff d f = 0.

LaTeX

$$$\text{If } weight w d < f.weightedOrder w,\ 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_eq_zero_of_lt_weightedOrder {d : σ →₀ ℕ} (h : (weight w d) < f.weightedOrder w) : coeff d f = 0 := by
  contrapose! h; exact weightedOrder_le w h

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