-
Notifications
You must be signed in to change notification settings - Fork 251
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: Ruzsa covering for sets #8916
Conversation
Add a version covering for `Set α` and `Nat.card`.
-- `norm_cast` would find these automatically, but breaks `to_additive` when it does so | ||
rw [←Finset.coe_mul, ←Finset.coe_mul, ←Finset.coe_div] | ||
norm_cast |
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.
@fpvandoorn, any ideas? It looks like norm_cast
is generating auxiliary lemmas, but the to_additive
tag isn't being transferred to them.
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.
This is not norm_cast
but lift
, it seems.
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.
I'd prefer to have an issue to reference in the comment about to_additive
before merging; perhaps Floris knows of one that already exists.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
I guess we can reference #1074 ? |
If we agree that we want to use |
bors r+ |
Add a version covering for `Set α` and `Nat.card`. From PFR Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Add a version covering for
Set α
andNat.card
.From PFR