mathlib3

ba169ae3 - feat(ring_theory/ideal/operations): the Third Isomorphism theorem for rings (#17243)

feat(ring_theory/ideal/operations): the Third Isomorphism theorem for rings (#17243) This wasn't much work - a "relative" version of the theorem had already been proven a while back (`ideal.quotient.quot_quot_equiv_quot_sup`) - but I think it's still worth having this version too (and explicitely marking it as being the Third Isomorphism theorem) Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>