-
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] - chore(data/fintype): generalise to_finset_card
#2316
Conversation
Why do you define it for finite types only? Quite a few properties (I mean the fact that fibers are equivalence classes of |
The main purpose of this work was to give me the fiber as a |
Co-authored-by: Reid Barton <rwbarton@gmail.com>
Okay, @urkud is completely right that it's silly to do this valued in This PR now contains:
|
to_finset_card
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.
Thanks 🎉
bors merge
Slight generalisation of a lemma, allowing a more flexible `fintype` instance. Also americanises some spelling. :-) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The sensitivity proof needs to be updated: https://github.com/leanprover-community/mathlib/pull/2316/checks?check_run_id=753840867#step:5:84 bors r- |
Canceled. |
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 merge
Slight generalisation of a lemma, allowing a more flexible `fintype` instance. Also americanises some spelling. :-) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
to_finset_card
to_finset_card
…y#2316) Slight generalisation of a lemma, allowing a more flexible `fintype` instance. Also americanises some spelling. :-) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Slight generalisation of a lemma, allowing a more flexible
fintype
instance.Also americanises some spelling. :-)