Skip to content

feat(Data/Finsupp): add computational lemmas for cons and single#35329

Open
BryceT233 wants to merge 11 commits intoleanprover-community:masterfrom
BryceT233:cons_eq_single
Open

feat(Data/Finsupp): add computational lemmas for cons and single#35329
BryceT233 wants to merge 11 commits intoleanprover-community:masterfrom
BryceT233:cons_eq_single

Conversation

@BryceT233
Copy link
Copy Markdown
Contributor

@BryceT233 BryceT233 commented Feb 15, 2026 •
edited
Loading

This PR introduces cons_injective2, cons_eq_single_zero_iff and cons_eq_single_succ_iff, which are helper lemmas designed to facilitate calculations (or simplification) of equalities involving Finsupp.cons and Finsupp.single.

Co-authored-by: Wenrong Zou [email protected]

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 15, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 15, 2026

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 15, 2026 •
edited
Loading

PR summary b301d257a1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ cons_eq_single_succ_iff
+ cons_eq_single_zero_iff
+ cons_injective2
+ cons_zero_eq_single_zero
+ cons_zero_single_eq_single_succ

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-data Data (lists, quotients, numbers, etc) label Feb 15, 2026
This was referenced Mar 12, 2026
Closed
Open
@mathlib-triage mathlib-triage bot assigned joneugster and unassigned TwoFX Mar 24, 2026
WenrongZou
WenrongZou reviewed Apr 1, 2026
View reviewed changes
@WenrongZou
Copy link
Copy Markdown
Contributor

WenrongZou commented Apr 2, 2026

LGTM! Thanks!

mathlib-bors bot pushed a commit that referenced this pull request Apr 2, 2026
@BryceT233
feat(Data/Finsupp): add lemmas for Finsupp and Sum (#36506)
c11f04c 
This PR adds various computational lemmas related to operations of finitely supported functions. Alongside #35329, theses lemmas provide the necessary helpers to construct various equivalences for `MvPowerSeries`.
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 3, 2026
@BryceT233 @xroblot
feat(Data/Finsupp): add lemmas for Finsupp and Sum (leanprover-co…
09c6519 
…mmunity#36506)

This PR adds various computational lemmas related to operations of finitely supported functions. Alongside leanprover-community#35329, theses lemmas provide the necessary helpers to construct various equivalences for `MvPowerSeries`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@WenrongZou WenrongZou WenrongZou left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@joneugster joneugster

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@BryceT233 @WenrongZou @TwoFX @joneugster