weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero

English

If p is less than the weighted order of f, then the weighted homogeneous component of weight p is zero.

Русский

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

LaTeX

$$$ p < f.weightedOrder\, w \Rightarrow f.weightedHomogeneousComponent\, w\, p = 0 $$$

Lean4

theorem weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero {f : MvPowerSeries σ R} {p : ℕ}
    (hf : p < f.weightedOrder w) : f.weightedHomogeneousComponent w p = 0 :=
  by
  ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · rw [coeff_zero]
    apply coeff_eq_zero_of_lt_weightedOrder w
    rw [hd]
    exact hf
  · rw [map_zero]

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