[Merged by Bors] - chore: add docs + alias for prod_bijective#8439
[Merged by Bors] - chore: add docs + alias for prod_bijective#8439
prod_bijective#8439Conversation
ericrbg
commented
Nov 16, 2023
| @[to_additive "`Fintype.sum_bijective` is a variant of `Finset.sum_bij` that accepts | ||
| `Function.bijective`. | ||
|
|
||
| See `Function.bijective.sum_comp` for a version without `h`. "] |
There was a problem hiding this comment.
Do you think we should rename this to finset_sum_comp to match?
There was a problem hiding this comment.
I think they're similar and will get discovered through each others' names, which IMO is good enough. Maybe we should point out that sum_comp is for the case where h is fun t => rfl.
There was a problem hiding this comment.
ah, that's what the "without h" means. I wonder if this one could get away with having e be implicit.
There was a problem hiding this comment.
@eric-wieser just to triple-check you're happy with the current state before I r+
|
✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with |
eric-wieser
left a comment
There was a problem hiding this comment.
bors merge
The renaming suggestion is really a follow-up suggestion anyway.
|
Pull request successfully merged into master. Build succeeded: |
prod_bijectiveprod_bijective