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(ring_theory): split finiteness into finite, finite type and finite presentation #17481
Conversation
As a side note, I think it would make more sense to move all the |
This PR/issue depends on: |
Looks like a very reasonable change to me. |
…inite presentation `module.finite` is used in a lot of places (especially in the form of `finite_dimensional`) but it is defined alongside `algebra.finite_type` and `algebra.finite_presentation`, so it brings a lot of dependencies with it. By splitting the file along the lines of the three definitions we should be able to clean up the import graph noticeably.
67ed307
to
79234cf
Compare
The dependencies for |
Thanks! bors d+ |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
Build passed, so: bors r+ |
👎 Rejected by label |
Try again: bors r+ |
…ite presentation (#17481) `module.finite` is used in a lot of places (especially in the form of `finite_dimensional`) but it is defined alongside `algebra.finite_type` and `algebra.finite_presentation`, so it brings a lot of dependencies with it. By splitting the file along the lines of the three definitions we should be able to clean up the import graph noticeably. In particular, finite dimensional vector spaces shouldn't know about (`mv_`)polynomials anymore.
Pull request successfully merged into master. Build succeeded: |
…17541) Theory on finitely generated submodules was defined in `ring_theory.noetherian`, but we can easily move it to `ring_theory.finiteness` which needs noticeably fewer imports. This move flips the import direction between the two files, since `finiteness` used to import `noetherian` and now it's the other way. Finally, some results that didn't fit neatly in either file are now in the new file `ring_theory.ideal.idempotent_fg`. As suggested in the discussion on #17481.
module.finite
is used in a lot of places (especially in the form offinite_dimensional
) but it is defined alongsidealgebra.finite_type
andalgebra.finite_presentation
, so it brings a lot of dependencies with it. By splitting the file along the lines of the three definitions we should be able to clean up the import graph noticeably. In particular, finite dimensional vector spaces shouldn't know about (mv_
)polynomials anymore.ring_theory.algebra_tower
#17480