mathlib3

a9dd84b4 - feat(ring_theory): specialize Chinese Remainder Theorem to two ideals (#17189)

feat(ring_theory): specialize Chinese Remainder Theorem to two ideals (#17189) The current arbitrarily-indexed version of CRT is surprisingly hard to apply to `R / (I ⊓ J)` inline, so here it is extracted into its own theorem. I added an import of the `fin_cases` tactic to `ring_theory.ideal.quotient`; I believe this is lightweight enough and certainly it wouldn't cause a big jump in the amount of transitive imports. Co-authored-by: Anne Baanen <t.baanen@vu.nl>