term_def₀ — Mathlib

English

If f(0) = 0, then term f s n = f(n) · (n)^{−s} for all s and n.

Русский

Если f(0) = 0, то term f s n = f(n) · (n)^{−s} для всех s и n.

LaTeX

$$$f(0) = 0 \\Rightarrow \\operatorname{term}(f,s,n) = f(n) \\cdot (n)^{-s}$$$

Lean4

/-- An alternate spelling of `term_def` for the case `f 0 = 0`. -/
theorem term_def₀ {f : ℕ → ℂ} (hf : f 0 = 0) (s : ℂ) (n : ℕ) : LSeries.term f s n = f n * (n : ℂ) ^ (-s) :=
  by
  rw [LSeries.term]
  split_ifs with h <;> simp [h, hf, cpow_neg, div_eq_inv_mul, mul_comm]

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