English
Let f,g: ℕ → ℂ and s ∈ ℂ. If hf,hg hold (L-series summable for f and g), then the L-series of f − g equals the difference of the L-series of f and g.
Русский
Пусть f,g : ℕ → ℂ и s ∈ ℂ. Если hf,hg выполняются (суммируемость L-рядов для f и g), то LSeries(f − g) s = LSeries f s − LSeries g s.
LaTeX
$$$\forall f,g:\mathbb{N}\to\mathbb{C},\ {s:\mathbb{C}},\ LSeriesSummable\,f\,s \Rightarrow LSeriesSummable\,g\,s \Rightarrow LSeries\,(f-g)\,s = LSeries\,f\,s - LSeries\,g\,s$$$
Lean4
@[simp]
theorem LSeries_sub {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_sub] using hf.tsum_sub hg
