Def Function.locallyFinsuppWithin.mk_of_mem_addSubgroup

Modification history

2026-03-12 21:45
Mathlib/Topology/LocallyFinsupp.lean
chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin (#35807) …
Added Function.locallyFinsuppWithin.mk_of_mem_addSubgroupView on Github →