mul — Mathlib

English

If f and g are multivariate power series homogeneous of degrees p and q, respectively, then their product f g is homogeneous of degree p+q.

Русский

Если f и g — многочлены-ряд ячейки MvPowerSeries и однородны степеней p и q соответственно, то их произведение f g однородно степени p+q.

LaTeX

$$$IsHomogeneous(f,p) \rightarrow IsHomogeneous(g,q) \rightarrow IsHomogeneous(f g, p+q)$$$

Lean4

protected theorem mul {f g : MvPowerSeries σ R} {p q : ℕ} (hf : f.IsHomogeneous p) (hg : g.IsHomogeneous q) :
    (f * g).IsHomogeneous (p + q) :=
  IsWeightedHomogeneous.mul hf hg

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