-
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/{multiset,finset}/pi): generalize from Type
to Sort
#18429
Conversation
604797b
to
01dfdb5
Compare
Also removes a duplicate lemma that was added by accident while porting.
Type
to Sort
Type
to Sort
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.
Well spotted! This looks reasonable, although we might want to move the material that's generalisable to Sort*
before the Type*
-specific one.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
I thought about that, but that seems more annoying to forward-port (and more importantly, review after forward-porting) |
It looks reasonable, but I'd rather let you merge it since I don't know the context w.r.t. mathport. bors d+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…18429) Everything in this file about `multiset.pi.cons` generalizes to `Sort`. The parts of the file which don't generalize now use `β` instead. This is motivated by #18417, though I do not know if supporting `Sort` is actually important there. Forward-ported as leanprover-community/mathlib4#2220
Pull request successfully merged into master. Build succeeded: |
Type
to Sort
Type
to Sort
This discard the changes from #18429, as these are already present in the new version.
Also removes a duplicate lemma that was added by accident while porting.
Also removes a duplicate lemma that was added by accident while porting.
Also removes a duplicate lemma that was added by accident while porting.
Everything in this file about
multiset.pi.cons
generalizes toSort
.The parts of the file which don't generalize now use
β
instead.This is motivated by #18417, though I do not know if supporting
Sort
is actually important there.Forward-ported as leanprover-community/mathlib4#2220