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