feat(linear_algebra/tensor_product): tensor product of finite modules is finite #13705
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
antoinelab01
added
the
awaiting-review
|
I have another proof at https://github.com/leanprover-community/mathlib/compare/tensor_fin_dim?expand=1 and I put it the instance in |
alreadydone
reviewed
Apr 26, 2022
|
|
||
| instance tensor_product.finite : module.finite R (M ⊗[R] N) := | ||
| { out := begin | ||
| rcases _inst_6.out with ⟨sM, hM⟩, |
There was a problem hiding this comment.
Try to avoid using _inst_6 explicitly, it is unstable since we do not control its name. You can write : ... := infer_instance or something like that. Same below.
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
2 tasks
alreadydone
removed
the
awaiting-review
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I'm not sure where to put
tensor_product.finite. It can't go inlinear_algebra/tensor_productbecause I cannot importring_theory/finitenessfrom there. I've put it intensor_product_basisfor now, let me know if you have a better idea of where it should go.