Commit 2026-02-03 14:54 eccf9629
View on Github →chore: improve notation in log counting function of Value Distribution Theory (#34250)
On a suggestion of @j-loreaux, improve notation by writing locallyFinsupp E ℤ instead of locallyFinsuppWithin (Set.univ : Set E) ℤ throughout Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean. Compactify some of the code in that file a little through trivial golfing.
Downgrade Function.locallyFinsupp in Mathlib/Topology/LocallyFinsupp.lean from a definition to an abbreviation, in order to use existing API without the constant need for typecast.