term — Mathlib

English

The nth term of the L-series is defined by term f s n = if n = 0 then 0 else f(n) / n^s.

Русский

n-й член L-рядa задаётся как term f s n = 0, если n = 0; иначе term f s n = f(n)/n^s.

LaTeX

$$$\\operatorname{term}(f,s,n) = \\begin{cases}0, & n=0 \\\\ \\dfrac{f(n)}{n^{s}}, & n\\neq 0\\end{cases}$$$

Lean4

/-- The `n`th term of the L-series of `f` evaluated at `s`. We set it to zero when `n = 0`. -/
noncomputable def term (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0 else f n / n ^ s

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