Theorem DirichletCharacter.LFunctionTrivChar₁_apply_one_ne_zero

Modification history

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