Theorem Function.locallyFinsuppWithin.coe_neg

Modification history

2026-03-12 21:45
Mathlib/Topology/LocallyFinsupp.lean
chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin (#35807) …
Modified Function.locallyFinsuppWithin.coe_negView 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.coe_negView on Github →