add — Mathlib

English

The sum of two homogeneous power series of the same weight p is homogeneous of weight p.

Русский

Сумма двух однородных рядов с одинаковым весом p остаётся однородной по весу p.

LaTeX

$$$ (f+g).IsHomogeneous p \Leftarrow f.IsHomogeneous p \\ and \\ g.IsHomogeneous p $$$

Lean4

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

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