add — Mathlib

English

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

Русский

Сумма двух взвешенно однородных рядов с одинаковым весом p снова взвешенно однородна по весу p.

LaTeX

$$$ (f,g) \text{ IsWeightedHomogeneous w p} \to (f+g) \text{ IsWeightedHomogeneous w p} $$$

Lean4

protected theorem add {f g : MvPowerSeries σ R} {p : ℕ} (hf : f.IsWeightedHomogeneous w p)
    (hg : g.IsWeightedHomogeneous w p) : (f + g).IsWeightedHomogeneous w p := fun {d} ↦
  by
  rw [not_imp_comm]
  intro hd
  rw [map_add, hf.coeff_eq_zero hd, hg.coeff_eq_zero hd, add_zero]

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