Commit 2020-07-23 07:50 d974457e

feat(ring_theory/ideal_over): a prime ideal lying over a maximal ideal is maximal (#3488) By making the results in ideal_over.lean a bit more general, we can transfer to quotient rings. This allows us to prove a strict inclusion I < J of ideals in S results in a strict inclusion I.comap f < J.comap f if R if f : R ->+* S is nice enough. As a corollary, a prime ideal lying over a maximal ideal is maximal.