powerSeriesFamily_add — Mathlib

English

The map powerSeriesFamily is additive in its second argument: the power series expansion of f+g equals the sum of the expansions of f and of g.

Русский

Карта powerSeriesFamily аддитивна по второму аргументу: разложение по степеням для f+g равно сумме разложений f и g.

LaTeX

$$$\\mathrm{powerSeriesFamily}\\ x\\ (f+g) = \\mathrm{powerSeriesFamily}\\ x\\ f + \\mathrm{powerSeriesFamily}\\ x\\ g$$$

Lean4

theorem powerSeriesFamily_add {x : HahnSeries Γ V} (f g : PowerSeries R) :
    powerSeriesFamily x (f + g) = powerSeriesFamily x f + powerSeriesFamily x g :=
  by
  ext1 n
  by_cases hx : 0 < x.orderTop <;> · simp [hx, add_smul]

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