Theorems · Theorem · number theory

LSeries_iteratedDeriv

∀ {f : ℕ → ℂ} (m : ℕ) {s : ℂ},
  LSeries.abscissaOfAbsConv f < ↑s.re → iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (LSeries.logMul^[m] f) s

If re s is greater than the abscissa of absolute convergence of f, then the mth derivative of this L-series is (-1)^m times the L-series of log^m * f.

Defined in

Mathlib.NumberTheory.LSeries.Deriv

Cited by

1 results in Mathlib

Foundations

Depth 297 from the axioms · uses propext, Classical.choice, Quot.sound