LSeries_congr — Mathlib

English

If f and g agree for all n ≠ 0, then LSeries f s = LSeries g s for any s.

Русский

Если f и g совпадают для всех n ≠ 0, то LSeries f s = LSeries g s при любом s.

LaTeX

$$$\\forall s,\\ \\bigl(\\forall n\\, (n \\neq 0 \\Rightarrow f(n) = g(n))\\bigr) \\Rightarrow LSeries(f,s) = LSeries(g,s)$$$

Lean4

/-- Congruence for `LSeries` with the evaluation variable `s`. -/
theorem LSeries_congr {f g : ℕ → ℂ} (h : ∀ {n}, n ≠ 0 → f n = g n) (s : ℂ) : LSeries f s = LSeries g s :=
  tsum_congr <| term_congr h s

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