Theorem locallyFinsuppWithin.logCounting_divisor

Modification history

2025-11-19 13:28
Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean
feat: describe the logarithmic counting function in terms of circle averages (#31583) …
Added locallyFinsuppWithin.logCounting_divisorView on Github →