proposition: Theorem chinese_remainder_prod : R / (I ⋅ J)%ideal ≅ (R / I) × (R / J).
proof: Proof. etransitivity. { rapply rng_quotient_invar. symmetry. rapply ideal_intersection_is_product. } rapply chinese_remainder. Defined.
imports: Classes.interfaces.abstract_algebra WildCat Modalities.ReflectiveSubuniverse Algebra.AbGroups Algebra.Rings.CRing Algebra.Rings.Ideal Algebra.Rings.QuotientRing