Commit 2024-12-02 11:22 17ec70ce

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 to RingTheory/Ideal/Operations.lean (the first place that they are used)
• results on ideal membership in RingTheory/Localization/Defs.lean go to RingTheory/Localization/Ideal.lean (idem)
• results on adjoining polynomials to a ring in Algebra/Polynomial/AlgebraMap.lean go to the new file RingTheory/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 from RingTheory/Polynomial/Basic.lean go to the new file RingTheory/Polynomial/Ideal.lean (merging this with RingTheory/Polynomial/Basic.lean is an okay option but would increase the downstream imports a lot)