Def Function.locallyFinsuppWithin.mk_of_mem

Modification history

2026-03-12 21:45
Mathlib/Topology/LocallyFinsupp.lean
chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin (#35807) …
Deleted Function.locallyFinsuppWithin.mk_of_memView on Github →
2025-03-25 19:36
Mathlib/Analysis/Meromorphic/Divisor/Basic.lean
feat: re-organize definition of divisors for meromorphic functions (#23302) …
Added Function.locallyFinsuppWithin.mk_of_memView on Github →