Commit 2022-11-14 12:00 ba169ae3

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)