Skip to content

[Merged by Bors] - feat: Set.sumEquiv lemmas#36268

Closed
smmercuri wants to merge 5 commits intoleanprover-community:masterfrom
smmercuri:setSumEquiv
Closed

[Merged by Bors] - feat: Set.sumEquiv lemmas#36268
smmercuri wants to merge 5 commits intoleanprover-community:masterfrom
smmercuri:setSumEquiv

Conversation

@smmercuri
Copy link
Copy Markdown
Collaborator

@smmercuri smmercuri commented Mar 6, 2026

Open in Gitpod

@smmercuri smmercuri added the WIP Work in progress label Mar 6, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 6, 2026 •
edited
Loading

PR summary d494882066

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ InjOn.sumElim
+ MapsTo.sumElim
+ sumEquiv_symm_apply

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).

@smmercuri smmercuri mentioned this pull request Mar 6, 2026
Open
9 tasks
@smmercuri smmercuri removed the WIP Work in progress label Mar 6, 2026
b-mehta
b-mehta reviewed Mar 6, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

Make sure you fix build, and also I guess you want to remove the commented bits?

b-mehta
b-mehta reviewed Mar 6, 2026
View reviewed changes
b-mehta
b-mehta approved these changes Mar 6, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

✌️ smmercuri can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 6, 2026
@smmercuri
Copy link
Copy Markdown
Collaborator Author

smmercuri commented Mar 6, 2026

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 6, 2026
@smmercuri
feat: Set.sumEquiv lemmas (#36268)
5e5be11
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Set.sumEquiv lemmas [Merged by Bors] - feat: Set.sumEquiv lemmas Mar 6, 2026
@mathlib-bors mathlib-bors bot closed this Mar 6, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 8, 2026
@smmercuri @xroblot
feat: Set.sumEquiv lemmas (leanprover-community#36268)
b1aeb18
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 9, 2026
@smmercuri @xroblot
feat: Set.sumEquiv lemmas (leanprover-community#36268)
e22e4f6
seewoo5 pushed a commit to seewoo5/mathlib4 that referenced this pull request Mar 9, 2026
@smmercuri @seewoo5
feat: Set.sumEquiv lemmas (leanprover-community#36268)
9ebc2e0
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@smmercuri @xroblot
feat: Set.sumEquiv lemmas (leanprover-community#36268)
9133cdb
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@smmercuri @b-mehta