coeff_weightedHomogeneousComponent

English

The coefficient at d of the weighted homogeneous component is equal to coeff d f if weight w d = p, otherwise it is zero.

Русский

Коэффициент при d взвешенного однородного компонента равен coeff d f при weight w d = p, иначе равен нулю.

LaTeX

$$$ \operatorname{coeff}_d( weightedHomogeneousComponent\ w\ p\ f ) = \begin{cases} \operatorname{coeff}_d f, & w(d) = p, \\ 0, & \text{иначе}. \end{cases} $$$

Lean4

theorem coeff_weightedHomogeneousComponent (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R) :
    coeff d (weightedHomogeneousComponent w p f) = if weight w d = p then coeff d f else 0 :=
  rfl

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