Commit 2026-03-12 21:45 c1a1f0d8

View on Github →

chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin (#35807) In this PR, we generalised the various instances for locally fin supp functions. These changes were originally made on the PR #26304 about algebraic cycles, but it was decided that these changes are more appropriate in their own PR.

Estimated changes

Modified Mathlib/Topology/LocallyFinsupp.lean

added theorem Function.locallyFinsupp.locallyFiniteSupport

modified theorem Function.locallyFinsuppWithin.coe_add

modified theorem Function.locallyFinsuppWithin.coe_neg

modified theorem Function.locallyFinsuppWithin.coe_nsmul

modified theorem Function.locallyFinsuppWithin.coe_sub

modified theorem Function.locallyFinsuppWithin.coe_zero

modified theorem Function.locallyFinsuppWithin.coe_zsmul

deleted def Function.locallyFinsuppWithin.mk_of_mem

added def Function.locallyFinsuppWithin.mk_of_mem_addSubgroup

added def Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid