homogeneousComponent_mul_of_le_order

English

If p ≤ f.order and q ≤ g.order, then the (p+q)-th homogeneous component of f g equals the product of the p-th and q-th homogeneous components.

Русский

Если p ≤ order(f) и q ≤ order(g), то (p+q)-я однородная компонента от f g равна произведению p-й и q-й однородных компонент.

LaTeX

$$p ≤ f.order → q ≤ g.order → homogeneousComponent(p+q)(f g) = homogeneousComponent(p) f * homogeneousComponent(q) g$$

Lean4

theorem homogeneousComponent_mul_of_le_order {f g : MvPowerSeries σ R} {p q : ℕ} (hf : p ≤ f.order) (hg : q ≤ g.order) :
    homogeneousComponent (p + q) (f * g) = homogeneousComponent p f * homogeneousComponent q g :=
  weightedHomogeneousComponent_mul_of_le_weightedOrder hf hg

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