proposition: Theorem chinese_remainder : R / (I ∩ J)%ideal ≅ (R / I) × (R / J).
proof: Proof. snrapply rng_first_iso'. 1: rapply rng_homo_crt. 1: exact _. apply ideal_subset_antisymm. - intros r [i j]. apply path_prod; apply qglue. 1: change (I (- r + 0)). 2: change (J (- r + 0)). 1,2: rewrite rng_plus_comm. 1,2: apply ideal_in_plus_negate. 1,3: apply ideal_in_zero. 1,2: assumption. - intros i p. apply equiv_path_prod in p. destruct p as [p q]. apply ideal_in_negate'. rewrite <- rng_plus_zero_r. split. 1: exact (related_quotient_paths _ _ _ p). 1: exact (related_quotient_paths _ _ _ q). Defined.
imports: Classes.interfaces.abstract_algebra WildCat Modalities.ReflectiveSubuniverse Algebra.AbGroups Algebra.Rings.CRing Algebra.Rings.Ideal Algebra.Rings.QuotientRing