Theorem Function.locallyFinsuppWithin.restrict_posPart

Modification history

2025-11-19 13:28
Mathlib/Topology/LocallyFinsupp.lean
feat: describe the logarithmic counting function in terms of circle averages (#31583) …
Added Function.locallyFinsuppWithin.restrict_posPartView on Github →