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: When Finsupp.prod
is nonzero
#8844
Conversation
Also replace `Finsupp.nonzero_iff_exists` by a more general lemma.
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.
Can you check if these lemma are consistent with DFinsupp
, and if not, adjust the dfinsupp ones too?
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Also replace `Finsupp.nonzero_iff_exists` by a more general lemma.
Canceled. |
bors merge |
Also replace `Finsupp.nonzero_iff_exists` by a more general lemma.
Pull request successfully merged into master. Build succeeded: |
Finsupp.prod
is nonzeroFinsupp.prod
is nonzero
Also replace `Finsupp.nonzero_iff_exists` by a more general lemma.
Also replace
Finsupp.nonzero_iff_exists
by a more general lemma.