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] - refactor(ring_theory/ideal/operations): split quotients to a new file #18531
Conversation
@@ -8,6 +8,7 @@ import algebra.algebra.restrict_scalars | |||
import algebra.algebra.subalgebra.basic | |||
import group_theory.finiteness | |||
import ring_theory.ideal.operations | |||
import ring_theory.ideal.quotient |
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 think you can avoid this import
by tweaking 1 proof a tiny little bit.
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.
Happy for me to do that as a follow-up? I agree that your proof in #18530 is nice here, but figure that it's fine to remain either in your PR or in another spin-off I can make tomorrow from https://github.com/leanprover-community/mathlib/tree/eric-wieser/finitenes-no-quotient (assuming it passes CI)
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.
Yes, please create a follow-up PR.
Thanks 🎉 bors merge |
…#18531) This file is growing quite long. Splitting it will reduce dependencies in (some) downstream files, and by becoming shorter also makes this file easier to edit and port. This doesn't attempt to change any proofs in downstream files; instead, it just adds new imports to keep them compiling. There are 9 downstream files which no longer depend on the `quotient_operations` file, although one of these now depends on `ring_theory.ideal.quotient`. A future PR will remove the `ring_theory.ideal.quotient_operations` import from more files. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This file is growing quite long.
Splitting it will reduce dependencies in (some) downstream files, and by becoming shorter also makes this file easier to edit and port.
This doesn't attempt to change any proofs in downstream files; instead, it just adds new imports to keep them compiling.
There are 9 downstream files which no longer depend on the
quotient_operations
file, although one of these now depends onring_theory.ideal.quotient
.A future PR will remove the
ring_theory.ideal.quotient_operations
import from more files.Split from #18530