Theorem DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv

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_LFunction_of_nontrivView on Github →