more questions about where to put lemmas

Stream: maths

[Anne Baanen]

I have a lemma that I would like to PR: ideal.comap_ne_bot_of_exists_root: let f : R -> S be a ring homomorphism and I an ideal of S. If I contains a root of a polynomial (nonzero) over R, then I.comap f is not the zero/bottom ideal. The main corollaries: ideal.comap_ne_bot_of_algebraic if S is algebraic over R (ideal.comap_integral_closure_ne_bot: specifically if S is the integral closure of R), its nonzero ideals lie over nonzero ideals in R.

Where should these results live? Since ring_theory.algebraic depends on ring_theory.integral_closure, and the dependencies in the proofs go exactly in the other direction, I'm leaning towards adding a new file.