-
Notifications
You must be signed in to change notification settings - Fork 297
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor(ring_theory/ideal/operations): split quotients to a new file (…
…#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>
- Loading branch information
1 parent
9a59dcb
commit e7f0ddb
Showing
8 changed files
with
520 additions
and
502 deletions.
There are no files selected for viewing
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
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
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
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
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
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
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