mathlib3

1f90e189 - feat(ring_theory/ideal_operations): Chinese Remainder Theorem (#774)