## Stream: maths

### Topic: more questions about where to put lemmas

#### Anne Baanen (Jul 07 2020 at 13:36):

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.

Last updated: May 09 2021 at 10:11 UTC