Commit 2021-01-20 06:40 385173df

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.