[Merged by Bors] - feat: Better lemmas for transferring finite sums along equivalences #9237
Conversation
Lemmas around this were a mess, throth in terms of names, statement and location. This PR standardises everything to be in `Algebra.BigOperators.Basic` and changes the lemmas to take in `InjOn` and `SurjOn` assumptions where possible (and where impossible make sure the hypotheses are taken in the correct order) and moves the equality of functions hypothesis last. Also add a few lemma that help fix downstream uses by golfing.
YaelDillies
added
awaiting-review
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| #align finset.equiv.sum_comp_finset Finset.Equiv.sum_comp_finset | ||
| -- TODO: Backport arguments changes to `card_congr` and `prod_bij` | ||
| @[to_additive] | ||
| lemma prod_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set ι).InjOn i) |
There was a problem hiding this comment.
What does the n in nbij stand for?
There was a problem hiding this comment.
Non-dependent. Bhavik came up with this name, we both don't like it. Do you have any suggestion?
There was a problem hiding this comment.
I'm inclined to go with prod_bij'. And just explain the difference in the docstrings using cross-refs. "See foo_bar for a (non)dependent variant."
There was a problem hiding this comment.
prod_bij' already exists! It's the version which takes in two functions that are inverse to each other on the finsets.
There was a problem hiding this comment.
Aha... arguably the name of that lemma should be closer to equiv than to bij. But maybe that's out of scope for this PR.
So let's go for nbij for now. But please explain the name in the docstrings.
|
!bench |
|
Here are the benchmark results for commit a7371c4. |
|
!bench |
|
Here are the benchmark results for commit 2089370. Benchmark Metric Change
======================================================
- ~Mathlib.Probability.StrongLaw instructions 10.3% |
|
|
|
bors d+ |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
bors merge |
…9237) Lemmas around this were a mess, throth in terms of names, statement and location. This PR standardises everything to be in `Algebra.BigOperators.Basic` and changes the lemmas to take in `InjOn` and `SurjOn` assumptions where possible (and where impossible make sure the hypotheses are taken in the correct order) and moves the equality of functions hypothesis last. Also add a few lemmas that help fix downstream uses by golfing. From LeanAPAP and LeanCamCombi
|
Build failed (retrying...): |
|
Canceled. |
|
bors merge |
…9237) Lemmas around this were a mess, throth in terms of names, statement and location. This PR standardises everything to be in `Algebra.BigOperators.Basic` and changes the lemmas to take in `InjOn` and `SurjOn` assumptions where possible (and where impossible make sure the hypotheses are taken in the correct order) and moves the equality of functions hypothesis last. Also add a few lemmas that help fix downstream uses by golfing. From LeanAPAP and LeanCamCombi
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Lemmas around this were a mess, throth in terms of names, statement and location. This PR standardises everything to be in
Algebra.BigOperators.Basicand changes the lemmas to take inInjOnandSurjOnassumptions where possible (and where impossible make sure the hypotheses are taken in the correct order) and moves the equality of functions hypothesis last.Also add a few lemmas that help fix downstream uses by golfing.
From LeanAPAP and LeanCamCombi