mathlib

d366eb3d - feat(ring_theory/ideal/operations): add some theorems about taking the quotient of a ring by a sum of ideals (#8668)

feat(ring_theory/ideal/operations): add some theorems about taking the quotient of a ring by a sum of ideals (#8668) The aim of this section is to prove that if `I, J` are ideals of the ring `R`, then the quotients `R/(I+J)` and `(R/I)/J'`are isomorphic, where `J'` is the image of `J` in `R/I`. Co-authored-by: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>