LSeries_add — Mathlib

English

If f and g are L-series summable at s, then LSeries(f+g) s = LSeries f s + LSeries g s.

Русский

Если f и g суммируемы по L-series в s, то LSeries(f+g) s = LSeries f s + LSeries g s.

LaTeX

$$$$ \mathrm{LSeries}(f+g)\, s = \mathrm{LSeries}(f)\, s + \mathrm{LSeries}(g)\, s. $$$$

Lean4

@[simp]
theorem LSeries_add {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) :
    LSeries (f + g) s = LSeries f s + LSeries g s := by simpa [LSeries, term_add] using hf.tsum_add hg

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