-
Notifications
You must be signed in to change notification settings - Fork 297
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(topology/algebra/module/multilinear): add continuous versions of constructions #18044
Conversation
… constructions One of these is a much more general case of `continuous_multilinear_map.curry0`; but to keep this PR small we don't attempt to remove `curry0`, instead just golfing it.
This PR/issue depends on: |
variables {M₂} | ||
variables (M₁) {M₂} |
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'm probably overlooking something obvious, but I can't see why you need M₁
to be explicit in const_of_is_empty
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.
How else would it be inferred?
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 asked that because you seem to always use _
to fill in this argument, which suggests that in all cases currently in mathlib the expected type is enough. But I get that in the middle of the proof it can be annoying to add a type annotation, so I'm okay with that.
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.
Ah, for this PR I needed the argument to state norm_const_of_is_empty
without needing @
or annotations
Thanks! |
🚀 Pull request has been placed on the maintainer queue by ADedecker. |
bors merge |
… constructions (#18044) One of these is a much more general case of `continuous_multilinear_map.curry0`; but to keep this PR small we don't attempt to remove `curry0`, instead just golfing it.
Pull request successfully merged into master. Build succeeded: |
One of these is a much more general case of
continuous_multilinear_map.curry0
; but to keep this PR small we don't attempt to removecurry0
, instead just golfing it.finset.prod_of_empty
#18045