-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(data/finset/finsupp): Finitely supported product of finsets #11639
Conversation
LGTM |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks for the quick review! bors merge |
) Define * `finsupp.indicator`: Similar to `finsupp.on_finset` except that it only requires a partially defined function. This is more compatible with `finset.pi`. * `finset.finsupp : finset ι → (ι → finset α) → finset (ι →₀ α)`: Finitely supported product of finsets. * `finsupp.pi : (ι →₀ finset α) → finset (ι →₀ α)`: The set of finitely supported functions whose `i`-th value lies in the `i`-th of a given `finset`-valued `finsupp`.
Build failed (retrying...): |
) Define * `finsupp.indicator`: Similar to `finsupp.on_finset` except that it only requires a partially defined function. This is more compatible with `finset.pi`. * `finset.finsupp : finset ι → (ι → finset α) → finset (ι →₀ α)`: Finitely supported product of finsets. * `finsupp.pi : (ι →₀ finset α) → finset (ι →₀ α)`: The set of finitely supported functions whose `i`-th value lies in the `i`-th of a given `finset`-valued `finsupp`.
Pull request successfully merged into master. Build succeeded: |
Define
finsupp.indicator
: Similar tofinsupp.on_finset
except that it only requires a partially defined function. This is more compatible withfinset.pi
.finset.finsupp : finset ι → (ι → finset α) → finset (ι →₀ α)
: Finitely supported product of finsets.finsupp.pi : (ι →₀ finset α) → finset (ι →₀ α)
: The set of finitely supported functions whosei
-th value lies in thei
-th of a givenfinset
-valuedfinsupp
.This is categorically pleasing.