Theorem DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁

Modification history

2024-11-20 17:06
Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
feat(NumberTheory/LSeries/DirichletContinuation): results on logarithmic derivatives (#19254) …
Added DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁View on Github →