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(ring_theory/finiteness): add finiteness of restrict_scalars #9363
Conversation
The analogous result for |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
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 d+
✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
We add `module.finitte.of_restrict_scalars_finite` and related lemmas: if `A` is an `R`-algebra and `M` is an `A`-module that is finite as `R`-module, then it is finite as `A`-module (similarly for `finite_type`).
Build failed (retrying...): |
We add `module.finitte.of_restrict_scalars_finite` and related lemmas: if `A` is an `R`-algebra and `M` is an `A`-module that is finite as `R`-module, then it is finite as `A`-module (similarly for `finite_type`).
Pull request successfully merged into master. Build succeeded: |
We add
module.finitte.of_restrict_scalars_finite
and related lemmas: ifA
is anR
-algebra andM
is anA
-module that is finite asR
-module, then it is finite asA
-module (similarly forfinite_type
).