OAI/NumberTheory/Ostmann/Characters/CharacterCompletedFiniteBound.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A finite nontrivial zero set would bound the completed logarithmic derivative
- theorem
OAI.Ostmann.completed_logDeriv_bounded_of_finite_zerosline 15