Commit 2021-11-10 14:52 f41854e8

feat(ring_theory/ideal/over): algebra structure on R/p → S/P for P lying over p (#9858) This PR shows P lies over p if there is an injective map completing the square R/p ← R —f→ S → S/P, and conversely that there is a (not necessarily injective, since f doesn't have to be) map completing the square if P lies over p. Then we specialize this to the case where P = map f p to provide an algebra p.quotient (map f p).quotient instance. This algebra instance is useful if you want to study the extension R → S locally at p, e.g. to show R/p : S/pS has the same dimension as Frac(R) : Frac(S) if p is prime.