Theorem DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one

Modification history

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