hurwitzZetaEven_def_of_ne_or_ne — Mathlib

English

If either a ≠ 0 or s ≠ 0, then hurwitzZetaEven a s equals completedHurwitzZetaEven a s divided by Gamma(s).

Русский

Если либо a ≠ 0, либо s ≠ 0, то hurwitzZetaEven a s равно completedHurwitzZetaEven a s делённому на Gamma(s).

LaTeX

$$$\\forall a:\\text{UnitAddCircle},\\ \\forall s:\\mathbb{C},\\ (a \\neq 0 \\lor s \\neq 0) \\\\Rightarrow\\ hurwitzZetaEven(a,s) = \\frac{\\mathrm{completedHurwitzZetaEven}(a,s)}{\\Gamma(s)}.$$$

Lean4

theorem hurwitzZetaEven_def_of_ne_or_ne {a : UnitAddCircle} {s : ℂ} (h : a ≠ 0 ∨ s ≠ 0) :
    hurwitzZetaEven a s = completedHurwitzZetaEven a s / Gammaℝ s :=
  by
  rw [hurwitzZetaEven]
  rcases ne_or_eq s 0 with h' | rfl
  · rw [Function.update_of_ne h']
  · simpa [Gammaℝ] using h

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