Commit 2024-12-02 11:22 17ec70ce
View on Github →chore(Algebra/Polynomial): don't import Ideal
when defining Polynomial.roots
(#19376)
This PR moves around a few definitions in order to free the definition of Polynomial.roots
of the knowledge of Ideal
. This was mostly motivated by writing assert_not_exists Ideal
in a few files and being amazed that it did exist.
In particular, the following changes are made:
- results involving ideals in
Algebra/Module/Submodule/Pointwise.lean
go toRingTheory/Ideal/Operations.lean
(the first place that they are used) - results on ideal membership in
RingTheory/Localization/Defs.lean
go toRingTheory/Localization/Ideal.lean
(idem) - results on adjoining polynomials to a ring in
Algebra/Polynomial/AlgebraMap.lean
go to the new fileRingTheory/Adjoin/Polynomial.lean
(I couldn't find an obvious place to put this:RingTheory/Adjoin/Basic.lean
does not know polynomials) - results on ideal membership in
Algebra/Polynomial/Div.lean
,Algebra/Polynomial/RingDivision.lean
and a few fromRingTheory/Polynomial/Basic.lean
go to the new fileRingTheory/Polynomial/Ideal.lean
(merging this withRingTheory/Polynomial/Basic.lean
is an okay option but would increase the downstream imports a lot)