mathlib3

d974457e - feat(ring_theory/ideal_over): a prime ideal lying over a maximal ideal is maximal (#3488)

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. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>