Skip to content

[Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin #35807

Closed
Raph-DG wants to merge 11 commits into
leanprover-community:masterfrom
Raph-DG:Raph-DG-locallyFinSuppInstances
Closed

[Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin #35807
Raph-DG wants to merge 11 commits into
leanprover-community:masterfrom
Raph-DG:Raph-DG-locallyFinSuppInstances

Conversation

@Raph-DG
Copy link
Copy Markdown
Collaborator

@Raph-DG Raph-DG commented Feb 26, 2026

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.

Open in Gitpod

@Raph-DG Raph-DG mentioned this pull request Feb 26, 2026
Open
3 tasks
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Feb 26, 2026 •
edited
Loading

PR summary 3e143864e8

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Function.locallyFinsupp.locallyFiniteSupport
+ addSubmonoid
+ instance [AddCommMonoid Y] : AddCommMonoid (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : AddGroup (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : SMul ℤ (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : Sub (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : Add (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : AddMonoid (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : SMul ℕ (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : Zero (locallyFinsuppWithin U Y)
+ memAddSubmonoid
+ mk_of_mem_addSubgroup
+ mk_of_mem_addSubmonoid
- instance [AddCommGroup Y] : Add (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : Neg (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : SMul ℕ (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : SMul ℤ (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : Sub (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : Zero (locallyFinsuppWithin U Y)

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Feb 26, 2026
dagurtomas
dagurtomas reviewed Mar 5, 2026
View reviewed changes
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
@dagurtomas dagurtomas added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 5, 2026
Raph-DG and others added 4 commits March 5, 2026 19:12
@Raph-DG @dagurtomas
Update Mathlib/Topology/LocallyFinsupp.lean
8989ec2 
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
@Raph-DG @dagurtomas
Update Mathlib/Topology/LocallyFinsupp.lean
21cfb9b 
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
@Raph-DG @dagurtomas
Update Mathlib/Topology/LocallyFinsupp.lean
077cba8 
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
@Raph-DG
Made name changes consistent and added in depricated lemma
57dfffc
@Raph-DG Raph-DG removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 5, 2026
dagurtomas
dagurtomas reviewed Mar 6, 2026
View reviewed changes
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
@dagurtomas
Copy link
Copy Markdown
Contributor

dagurtomas commented Mar 12, 2026

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Mar 12, 2026

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

trigger_name: issue_comment
wf_run: workflow_run

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 12, 2026
j-loreaux
j-loreaux reviewed Mar 12, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors merge

@mathlib-triage mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 12, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Mar 12, 2026
@Raph-DG
chore(Topology): Generalised some of the instances for Function.local…
c1a1f0d 
…lyFinsuppWithin (#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.

Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Mar 12, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin [Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin Mar 12, 2026
@mathlib-bors mathlib-bors Bot closed this Mar 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

@dagurtomas dagurtomas dagurtomas left review comments

Assignees

@dagurtomas dagurtomas

Labels

ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Raph-DG @dagurtomas @j-loreaux