mathlib3

385173df - feat(ring_theory/ideal/operations): generalize quotient of algebras (#5802)

feat(ring_theory/ideal/operations): generalize quotient of algebras (#5802) I generalize #5703 (that was merged earlier today... sorry for that, I should have thought more carefully about it) to be able to work with `S/I` as an `R`-algebra, where `S` is an `R`-algebra. (In #5703 only `R/I` was considered.) The proofs are the same.