homogeneousComponent_of_lt_order_eq_zero

English

If p is less than the order of f, then the p-th homogeneous component of f is zero.

Русский

Если p меньше порядка f, то p-я однородная компонента f равна нулю.

LaTeX

$$p < f.order → homogeneousComponent(p) f = 0$$

Lean4

theorem homogeneousComponent_of_lt_order_eq_zero {f : MvPowerSeries σ R} {p : ℕ} (hf : p < f.order) :
    f.homogeneousComponent p = 0 :=
  weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero hf

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