Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.zetaTimesSMinusOne_entire_differentiable

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:512 to 521

Source documentation

The removable extension of (s - 1)ζ(s) is entire.

Exact Lean statement

theorem zetaTimesSMinusOne_entire_differentiable :
    Differentiable ℂ zetaTimesSMinusOne_entire

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaTimesSMinusOne_entire_differentiable :    Differentiable ℂ zetaTimesSMinusOne_entire := by  have hiff :=    (Complex.differentiableOn_compl_singleton_and_continuousAt_iff (f := zetaTimesSMinusOne_entire)      (s := (Set.univ : Set ℂ)) (c := (1 : ℂ)) (by simp))  have : DifferentiableOn ℂ zetaTimesSMinusOne_entire (Set.univ : Set ℂ) :=    hiff.1      ⟨zetaTimesSMinusOne_entire_differentiableOn_compl_singleton,        zetaTimesSMinusOne_entire_continuousAt_one⟩  simpa [DifferentiableOn, differentiableWithinAt_univ, zetaTimesSMinusOne_entire] using! this