theorem proved term proof

`completedZeta0_differentiable`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  30theorem completedZeta0_differentiable :
  31    Differentiable ℂ completedRiemannZeta₀ :=

Term-mode proof.

  32  differentiable_completedZeta₀
  33
  34/-- The pole-removed completed zeta has the same functional equation. -/

From the project-wide theorem graph. These declarations reference this one in their body.

hadamardFactorizationStatus in IndisputableMonolith.NumberTheory.HadamardFactorization decl_use

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
zeta in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use