Commit 2020-07-13 20:02 11322372

feat(ring_theory/ideal_over): lemmas for nonzero ideals lying over nonzero ideals (#3385) Let f be a ring homomorphism from R to S and I be an ideal in S. To show that I.comap f is not the zero ideal, we can show I contains a non-zero root of some non-zero polynomial p : polynomial R. As a corollary, if S is algebraic over R (e.g. the integral closure of R), nonzero ideals in S lie over nonzero ideals in R. I created a new file because integral_closure.comap_ne_bot depends on comap_ne_bot_of_algebraic_mem, but ring_theory/algebraic.lean imports ring_theory/integral_closure.lean and I didn't see any obvious join in the dependency graph where they both belonged.