R / (I ∩ J)%ideal ≅ (R / I) × (R / J). 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.
Require Import Classes.interfaces.canonical_names. Require Import WildCat. Require Import Modalities.ReflectiveSubuniverse. Require Import Algebra.AbGroups. Require Import Algebra.Rings.Ring. Require Import Algebra.Rings.Ideal. Require Import Algebra.Rings.QuotientRing. Require Import Algebra.Rings.CRing. Import Ideal.Notation.